| Publication | Date of Publication | Type |
|---|
| Compositional reversible computation | 2024-11-13 | Paper |
| A machine-checked proof of Birkhoff's variety theorem in Martin-Löf type theory | 2024-08-01 | Paper |
From reversible programs to univalent universes and back
(available as arXiv preprint) | 2022-04-25 | Paper |
Fractional types. Expressive and safe space management for ancilla bits
(available as arXiv preprint) | 2021-07-05 | Paper |
Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
The Mathematical Intelligencer | 2021-04-19 | Paper |
| A Machine-checked proof of Birkhoff's Variety Theorem in Martin-L\"of Type Theory | 2021-01-25 | Paper |
Leveraging the information contained in theory presentations
(available as arXiv preprint) | 2021-01-20 | Paper |
Towards specifying symbolic computation
(available as arXiv preprint) | 2020-01-22 | Paper |
| Building on the Diamonds between Theories: Theory Presentation Combinators | 2018-12-14 | Paper |
| Embracing the Laws of Physics: Three Reversible Models of Computation | 2018-11-08 | Paper |
Biform theories: project description
(available as arXiv preprint) | 2018-10-18 | Paper |
| A library of reversible circuit transformations (work in progress) | 2018-10-17 | Paper |
HOL Light QE
(available as arXiv preprint) | 2018-10-04 | Paper |
| From high-level inference algorithms to efficient code | 2018-05-16 | Paper |
Formalizing mathematical knowledge as a biform theory graph: a case study
(available as arXiv preprint) | 2017-07-21 | Paper |
Computing with semirings and weak rig groupoids
Programming Languages and Systems | 2016-04-26 | Paper |
Probabilistic inference by program transformation in Hakaru (system description)
Functional and Logic Programming | 2016-04-04 | Paper |
Realms: a structure for consolidating knowledge about mathematical theories
Lecture Notes in Computer Science | 2014-08-07 | Paper |
Theory presentation combinators
Lecture Notes in Computer Science | 2012-09-07 | Paper |
MathScheme: project description
Lecture Notes in Computer Science | 2011-07-29 | Paper |
Partial evaluation of Maple
Science of Computer Programming | 2011-05-04 | Paper |
Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code
Science of Computer Programming | 2011-05-04 | Paper |
Symbolic domain decomposition
Lecture Notes in Computer Science | 2010-08-24 | Paper |
Mechanized Mathematics
Lecture Notes in Computer Science | 2010-08-24 | Paper |
Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
Journal of Functional Programming | 2009-11-13 | Paper |
A Review of Mathematical Knowledge Management
Lecture Notes in Computer Science | 2009-07-09 | Paper |
Bimonadic Semantics for Basic Pattern Matching Calculi
Lecture Notes in Computer Science | 2009-04-02 | Paper |
High-Level Theories
Lecture Notes in Computer Science | 2009-01-27 | Paper |
| scientific article; zbMATH DE number 5494025 (Why is no real title available?) | 2009-01-20 | Paper |
| scientific article; zbMATH DE number 5286863 (Why is no real title available?) | 2008-06-11 | Paper |
| Computing properties of numerical imperative programs by symbolic computation | 2008-01-02 | Paper |
A Rational Reconstruction of a System for Experimental Mathematics
Towards Mechanized Mathematical Assistants | 2007-11-28 | Paper |
Relational Methods in Computer Science
Lecture Notes in Computer Science | 2007-05-02 | Paper |
Gaussian elimination: a case study in efficient genericity with MetaOCaml
Science of Computer Programming | 2006-10-05 | Paper |
| scientific article; zbMATH DE number 2145000 (Why is no real title available?) | 2005-03-14 | Paper |
