I am a maths and computer science PhD student. I currently live in Brussels.
You can email me at antvanmul then at then hotmail then .com.
My office at KU Leuven is 200A (cs building), 03.127.
I am a maths and computer science PhD student. I currently live in Brussels.
You can email me at antvanmul then at then hotmail then .com.
My office at KU Leuven is 200A (cs building), 03.127.
I am a PhD student working with Dominique Devriese and Andreas Nuyts at KU Leuven. My research is about parametricity for dependent type theories. An explainer about parametricity appears at the end of this webpage.
Before that, I was working as a research engineer at Inria Paris in the Prosecco team, where the F* Verification Language for Effectful Programs is/was being developed. I did my master internship with Catalin Hritcu in the same team (link).
I hold a bachelor's degree in mathematics from Université Libre de Bruxelles, and a master's degree in mathematical logic and theoretical computer science from Université de Paris.
I am interested in mathematical unifying theories for logic, computer science, algebra and geometry, as well as in those topics themselves. Here is a non-exhaustive list:
Briefly speaking parametricity is the fact that, types of a programming language are more than sets: types ought to be seen as "reflexive graphs". In other words a type contains values, and possibly edges between values. Typically there is an edge between values v₀, v₁ if v₀ and v₁ have the same "structure". What that means depends on the type of v₀, v₁. For instance if v₀, v₁ are lists of the same size, an edge between v₀, v₁ is a list of edges between the values stored in v₀, v₁. Another example of edge: there is always an edge between a value v and itself, this is what "reflexive" means above.
The same way types are reflexive graphs, programs p : A → B are morphisms of reflexive graphs, so maps that send values to values, but also edges to edges. More precisely, assume (p : A → B), (a₀, a₁ : A) and an edge (e : Edge A a₀ a₁). Then there is an edge in B, between the values p(a₀) and p(a₁). One way to understand this property is: in the presence of parametricity, programs map structurally related values to structurally related values.
Roughly, the latter is the reason why parametricity on one side and classical principles on the other (law of excluded middle, axiom of choice) are incompatible. Here is the law of excluded middle as a program p : (A : Statement) → A or ¬A. From a programming point of view, it is a procedure that given a statement A decides whether A is provable or not. Using parametricity it is possible to prove that no such procedure p exists.