Meven Lennon-Bertrand

Work

University of Cambridge
|

Research Associate (Postdoctoral Researcher)

United Kingdom of Great Britain and Northern Ireland

→

Université de Nantes
|

PhD Student

France

→

ENS de Lyon
|

Normalien élève

France

→

Education

Nantes Université
France

→

PhD

ENS de Lyon
France

→

Master

ENS de Lyon
France

→

Master

Radboud University
Netherlands

→

Erasmus, Master

ENS de Lyon
France

→

Licence (Bachelor)

Université de Lyon
France

→

Licence (Bachelor)

Publications

Correct and Complete Type Checking and Certified Erasure for Coq , in Coq

Published by

Journal of the ACM

Summary

journal-article

Martin-Löf à la Coq

Published by

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs

Summary

conference-paper

Artifact Description – Definitional Functoriality for Dependent (Sub)Types

Published by

Programming Languages and Systems

Summary

software

Definitional Functoriality for Dependent (Sub)Types

Summary

book-chapter

A reasonably gradual type theory

Published by

Proceedings of the ACM on Programming Languages

Summary

journal-article

A reasonably gradual type theory

Published by

Proceedings of the ACM on Programming Languages

Summary

journal-article

Gradualizing the Calculus of Inductive Constructions

Published by

ACM Transactions on Programming Languages and Systems

Summary

journal-article

Complete Bidirectional Typing for the Calculus of Inductive Constructions

Published by

Interactive Theorem Proving (ITP)

Summary

journal-article