BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Sozeau:Matthieu

Contributed to:

ICFP 20152015
LICS 20122012
POPL 20192019
POPL 20202020

Wrote 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.
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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.