| Publication | Date of Publication | Type |
|---|
The Rewster: type preserving rewrite rules for the Rocq Prover. Extended version of the ITP 2024 paper
Journal of Automated Reasoning | 2026-05-28 | Paper |
Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}
Journal of the ACM | 2026-02-24 | Paper |
| The rewster: type preserving rewrite rules for the Coq proof assistant | 2026-02-10 | Paper |
The Marriage of Univalence and Parametricity
Journal of the ACM | 2022-12-08 | Paper |
Model structure on the universe of all types in interval type theory
Mathematical Structures in Computer Science | 2022-01-20 | Paper |
| An effectful way to eliminate addiction to dependence | 2021-01-19 | Paper |
The \textsc{MetaCoq} project
Journal of Automated Reasoning | 2020-11-02 | Paper |
| Setoid type theory -- a syntactic translation | 2020-05-05 | Paper |
| Lawvere-Tierney sheafification in Homotopy Type Theory | 2019-09-18 | Paper |
| Failure is not an option. An exceptional type theory | 2019-09-13 | Paper |
Chemical foundations of distributed aspects
Distributed Computing | 2019-07-11 | Paper |
| Towards certified meta-programming with typed Template-Coq | 2018-10-04 | Paper |
An explicit formula for the free exponential modality of linear logic
Mathematical Structures in Computer Science | 2018-08-07 | Paper |
Foundations of dependent interoperability
Journal of Functional Programming | 2018-08-03 | Paper |
The definitional side of the forcing
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
A Contraction Theory Approach to Stochastic Incremental Stability
IEEE Transactions on Automatic Control | 2017-08-08 | Paper |
| Wild \(\omega\)-categories for the homotopy hypothesis in type theory | 2017-07-12 | Paper |
Extending type theory with forcing
2012 27th Annual IEEE Symposium on Logic in Computer Science | 2017-05-16 | Paper |
Partial type equivalences for verified dependent interoperability
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming | 2017-05-10 | Paper |
An algebraic account of references in game semantics
Electronic Notes in Theoretical Computer Science | 2016-05-10 | Paper |
Kripke open bisimulation. A marriage of game semantics and operational techniques
Programming Languages and Systems | 2016-01-08 | Paper |
Universe polymorphism in Coq
Interactive Theorem Proving | 2014-09-08 | Paper |
| Contraction analysis of nonlinear random dynamical systems | 2013-09-20 | Paper |
Resource modalities in tensor logic
Annals of Pure and Applied Logic | 2011-08-26 | Paper |
An Explicit Formula for the Free Exponential Modality of Linear Logic
Automata, Languages and Programming | 2009-07-14 | Paper |
Geometry of the superior colliculus mapping and efficient oculomotor computation
Biological Cybernetics | 2007-11-12 | Paper |
Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
Lecture Notes in Computer Science | 2005-08-19 | Paper |
