Matthieu Sozeau

Registered user since Mon 18 Apr 2016

Name:Matthieu Sozeau
Country:France
Affiliation:Inria
Personal website:http://mattam.org
Research interests:Type Theory, Proof Assistants, Functional Programming, Unification

Contributions

ML 2022 Author of Extraction to OCaml from Coq: Operational Correctness Verified in Coq within the ML-track
CoqPL 2022 Speaker of Session with the Coq Development Team within the CoqPL-track
WITS 2022 Author of The curious case of case: correct & efficient representation of case analysis in Coq and MetaCoq within the WITS 2022-track
POPL 2021 Committee Member in Program Committee within the POPL-track
CoqPL 2021 Presenter of Session with the Coq Development Team within the CoqPL-track
CoqPL 2020 Author of Session with the Coq Development Team within the CoqPL-track
Author of A Tutorial on Equations within the CoqPL-track
POPL 2020 Author of Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq within the Research Papers-track
ICFP 2019 Committee 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
POPL 2019 Author of Definitional Proof-Irrelevance without K within the Research Papers-track
CPP 2019 Author of Eliminating Reflection from Type Theory within the CPP 2019-track
CoqPL 2019 Author 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
ICFP 2018 Author of Equivalences for Free: Univalent Parametricity for Effective Transport within the Research Papers-track
TyDe 2018 Committee Member in Program Committee within the TyDe 2018-track
CoqPL 2018 Author of Typed Template Coq within the -track
Author of Session with the Coq Development Team within the -track
PEPM 2018 Author of Equations: From Clauses to Splittings to Functions (Poster/Demo Talk) within the PEPM 2018-track
CoqPL 2017 Session 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
CPP 2017 Author of The HoTT library: a formalization of homotopy type theory in Coq within the CPP-track
TTT 2017 Author of Equations: a tool for dependent pattern-matching within the TTT-track
CoqPL 2016 Author of Coq 8.5 at work and the future of Coq within the CoqPL-track
Committee Member in Program Committee within the CoqPL-track