| Publication | Date of Publication | Type |
|---|
Structured monads for generic first-order syntax metatheory
Journal of Automated Reasoning | 2025-10-22 | Paper |
Choice trees: representing and reasoning about nondeterministic, recursive, and impure programs in Rocq
Journal of Functional Programming | 2025-10-10 | Paper |
| Syntax monads for the working formal metatheorist | 2025-08-05 | Paper |
| Tealeaves: structured monads for generic first-order abstract syntax infrastructure | 2024-11-26 | Paper |
scientific article; zbMATH DE number 7809762 (Why is no real title available?)
(available as arXiv preprint) | 2024-02-27 | Paper |
| scientific article; zbMATH DE number 7809762 (Why is no real title available?) | 2024-02-27 | Paper |
| scientific article; zbMATH DE number 7699449 (Why is no real title available?) | 2023-06-20 | Paper |
scientific article; zbMATH DE number 7439427 (Why is no real title available?)
(available as arXiv preprint) | 2021-12-06 | Paper |
| scientific article; zbMATH DE number 7439427 (Why is no real title available?) | 2021-12-06 | Paper |
Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces
Scientific Annals of Computer Science | 2019-02-08 | Paper |
| A formal equational theory for call-by-push-value | 2018-10-04 | Paper |
A linear/producer/consumer model of classical linear logic
Mathematical Structures in Computer Science | 2018-04-25 | Paper |
| An axiomatic specification for sequential memory models | 2018-03-01 | Paper |
Downgrading policies and relaxed noninterference
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2017-07-14 | Paper |
Example-directed synthesis: a type-theoretic interpretation
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2016-10-24 | Paper |
Principals in programming languages, a syntactic proof technique
Proceedings of the fourth ACM SIGPLAN international conference on Functional programming | 2016-09-01 | Paper |
Linear is CP (more or less)
A List of Successes That Can Change the World | 2016-08-17 | Paper |
| A type system for robust declassification | 2016-05-03 | Paper |
Formalizing the LLVM intermediate representation for verified program transformations
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-09-11 | Paper |
AURA
Proceedings of the 13th ACM SIGPLAN international conference on Functional programming | 2015-03-16 | Paper |
Translating dependency into parametricity
Proceedings of the ninth ACM SIGPLAN international conference on Functional programming | 2015-03-09 | Paper |
Lolliproc: to concurrency from classical linear logic via Curry-Howard and control
Proceedings of the 15th ACM SIGPLAN international conference on Functional programming | 2015-03-05 | Paper |
Finite vector spaces as model of simply-typed lambda-calculi
Theoretical Aspects of Computing – ICTAC 2014 | 2015-01-13 | Paper |
A core quantitative coeffect calculus
Programming Languages and Systems | 2014-04-16 | Paper |
Generative type abstraction and type-level computation
Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-04-10 | Paper |
Mechanized verification of computing dominators for formalizing compilers
Certified Programs and Proofs | 2013-04-19 | Paper |
Arrows for secure information flow
Theoretical Computer Science | 2010-04-22 | Paper |
Preserving Secrecy Under Refinement
Automata, Languages and Programming | 2007-09-11 | Paper |
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science | 2006-07-06 | Paper |
Programming Languages and Systems
Lecture Notes in Computer Science | 2005-09-13 | Paper |
Secure information flow via linear continuations
Higher-Order and Symbolic Computation | 2003-05-14 | Paper |
| scientific article; zbMATH DE number 1692933 (Why is no real title available?) | 2002-01-21 | Paper |
