Travelled to:1 × Canada
1 × Croatia
Collaborated with:N.Tabareau B.Ziliani G.Jaber Gaëtan Gilbert J.Cockx Simon Boulier Yannick Forster 0002 Théo Winterhalter
Talks about:coq (5) type (2) polymorph (1) algorithm (1) overload (1) without (1) univers (1) irrelev (1) definit (1) correct (1)
Person: Matthieu Sozeau
DBLP: Sozeau:Matthieu
Contributed to:
2015
2012
20192020Wrote 4 papers:
- ICFP-2015-ZilianiS #algorithm #coq #morphism #polymorphism #unification
- A unification algorithm for Coq featuring universe polymorphism and overloading (BZ, MS), pp. 179–191.
- LICS-2012-JaberTS #type system
- Extending Type Theory with Forcing (GJ, NT, MS), pp. 395–404.
- POPL-2019-GilbertCST
- Definitional proof-irrelevance without K (GG, JC, MS, NT), p. 28.
- POPL-2020-SozeauBFTW #coq #exclamation #type checking #verification
- Coq Coq correct! verification of type checking and erasure for Coq, in Coq (MS, SB, YF0, NT, TW), p. 28.