| Publication | Date of Publication | Type |
|---|
| Multirole Logic (Extended Abstract) | 2017-03-19 | Paper |
Guarded recursive datatype constructors
Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-09-11 | Paper |
Meta-programming through typeful code representation
Proceedings of the eighth ACM SIGPLAN international conference on Functional programming | 2015-07-02 | Paper |
A dependently typed assembly language
Proceedings of the sixth ACM SIGPLAN international conference on Functional programming | 2015-03-09 | Paper |
Combining programming with theorem proving
Proceedings of the tenth ACM SIGPLAN international conference on Functional programming | 2015-01-06 | Paper |
| A formalization of strong normalization for simply-typed lambda-calculus and System F | 2014-01-10 | Paper |
| scientific article; zbMATH DE number 5872266 (Why is no real title available?) | 2011-03-30 | Paper |
| ATS/LF: A type system for constructing proofs as total functional programs | 2011-03-30 | Paper |
A modality for safe resource sharing and code reentrancy
Lecture Notes in Computer Science | 2010-08-31 | Paper |
A simple and general theoretical account for abstract types
Lecture Notes in Computer Science | 2009-12-09 | Paper |
Attributive Types for Proof Erasure
Lecture Notes in Computer Science | 2008-06-03 | Paper |
Dependent ML An approach to practical programming with dependent types
Journal of Functional Programming | 2007-09-26 | Paper |
Frontiers of Combining Systems
Lecture Notes in Computer Science | 2006-10-10 | Paper |
| scientific article; zbMATH DE number 5033864 (Why is no real title available?) | 2006-06-19 | Paper |
Types for Proofs and Programs
Lecture Notes in Computer Science | 2005-12-23 | Paper |
Meta-programming through typeful code representation
Journal of Functional Programming | 2005-11-28 | Paper |
| scientific article; zbMATH DE number 2185727 (Why is no real title available?) | 2005-07-04 | Paper |
Dependent types for program termination verification
Higher-Order and Symbolic Computation | 2002-12-15 | Paper |
Upper bounds for standardizations and an application
Journal of Symbolic Logic | 2000-06-22 | Paper |
Perpetual reductions in \(\lambda\)-calculus
Information and Computation | 1999-09-09 | Paper |
| scientific article; zbMATH DE number 1114357 (Why is no real title available?) | 1998-06-01 | Paper |
| scientific article; zbMATH DE number 1088210 (Why is no real title available?) | 1997-11-17 | Paper |
TPS: A theorem-proving system for classical type theory
Journal of Automated Reasoning | 1996-11-25 | Paper |
| scientific article; zbMATH DE number 4125387 (Why is no real title available?) | 1988-01-01 | Paper |
