Matthieu Sozeau

Registered user since Mon 18 Apr 2016

Name: Matthieu Sozeau

Country: France

Affiliation: Inria

Personal website: http://www.pps.univ-paris-diderot.fr/~sozeau/

Research interests: Type Theory, Proof Assistants, Functional Programming, Unification

Contributions

CoqPL 2020Author of Session with the Coq Development Team within the CoqPL-track
Author of A Tutorial on Equations within the CoqPL-track
POPL 2020Author of Coq Coq Correct: Verification of Type Checking and Erasure for Coq, in Coq within the Research Papers-track
CoqPL 2019Author of Session with the Coq Development Team within the CoqPL-track
Author of Reification of Shallow-Embedded DSLs in Coq with Automated Verification within the CoqPL-track
CPP 2019Author of Eliminating Reflection from Type Theory within the CPP 2019-track
POPL 2019Author of Definitional Proof-Irrelevance without K within the Research Papers-track
TyDe 2018Committee Member in Program Committee within the TyDe 2018-track
ICFP 2019Committee Member in External Review Committee within the Research Papers-track
Author of Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq within the Research Papers-track
CoqPL 2018Author of Typed Template Coq within the -track
Author of Session with the Coq Development Team within the -track
PEPM 2018Author of Equations: From Clauses to Splittings to Functions (Poster/Demo Talk) within the PEPM 2018-track
ICFP 2018Author of Equivalences for Free: Univalent Parametricity for Effective Transport within the Research Papers-track
CPP 2017Author of The HoTT library: a formalization of homotopy type theory in Coq within the CPP-track
TTT 2017Author of Equations: a tool for dependent pattern-matching within the TTT-track
CoqPL 2017Session Chair of Afternoon Session (part of CoqPL 2017)
Author of CertiCoq: A verified compiler for Coq within the CoqPL 2017-track
Committee Member in Program Committee within the CoqPL 2017-track
Author of Session with the Coq Development Team within the CoqPL 2017-track
CoqPL 2016Author of Coq 8.5 at work and the future of Coq within the CoqPL-track
Committee Member in Program Committee within the CoqPL-track