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