| Publication | Date of Publication | Type |
|---|
| Dependent type refinements for futures | 2026-04-02 | Paper |
| Data layout from a type-theoretic perspective | 2026-04-02 | Paper |
| Type-based termination for futures | 2024-05-27 | Paper |
Manifest deadlock-freedom for shared session types
Programming Languages and Systems | 2023-11-24 | Paper |
A logical framework with higher-order rational (circular) terms
Lecture Notes in Computer Science | 2023-11-24 | Paper |
Polarized subtyping
Programming Languages and Systems | 2023-08-03 | Paper |
| Presenting intuitive deductions via symmetric simplification | 2023-04-28 | Paper |
| The TPS theorem proving system | 2023-04-28 | Paper |
Inductively defined types in the Calculus of Constructions
Lecture Notes in Computer Science | 2023-04-12 | Paper |
The practice of logical frameworks
Trees in Algebra and Programming — CAAP '96 | 2023-02-23 | Paper |
scientific article; zbMATH DE number 7649947 (Why is no real title available?)
(available as arXiv preprint) | 2023-02-03 | Paper |
Circular proofs as session-typed processes: a local validity condition
(available as arXiv preprint) | 2022-08-02 | Paper |
| Circular proofs as session-typed processes: a local validity condition | 2022-08-02 | Paper |
Session Types with Arithmetic Refinements
(available as arXiv preprint) | 2022-07-18 | Paper |
Back to futures
Journal of Functional Programming | 2022-03-17 | Paper |
A linear logic of authorization and knowledge
Computer Security – ESORICS 2006 | 2022-03-09 | Paper |
scientific article; zbMATH DE number 7471698 (Why is no real title available?)
(available as arXiv preprint) | 2022-02-09 | Paper |
| scientific article; zbMATH DE number 7471698 (Why is no real title available?) | 2022-02-09 | Paper |
| scientific article; zbMATH DE number 7441269 (Why is no real title available?) | 2021-12-08 | Paper |
scientific article; zbMATH DE number 7441269 (Why is no real title available?)
(available as arXiv preprint) | 2021-12-08 | Paper |
Session-typed concurrent contracts
Journal of Logical and Algebraic Methods in Programming | 2021-11-24 | Paper |
Nested session types
(available as arXiv preprint) | 2021-10-18 | Paper |
| A universal session type for untyped asynchronous communication | 2021-08-04 | Paper |
A message-passing interpretation of adjoint logic
Journal of Logical and Algebraic Methods in Programming | 2021-06-25 | Paper |
Work analysis with resource-aware session types
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
Elf: A meta-language for deductive systems
Automated Deduction — CADE-12 | 2020-01-21 | Paper |
Session-typed concurrent contracts
Programming Languages and Systems | 2019-09-13 | Paper |
A probabilistic language based upon sampling functions
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2017-07-14 | Paper |
Contextual modal type theory
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
On equivalence and canonical forms in the LF type theory
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Higher-order pattern complement and the strict \(\lambda\)-calculus
ACM Transactions on Computational Logic | 2017-06-13 | Paper |
Substructural proofs as automata
Programming Languages and Systems | 2016-12-21 | Paper |
Monitors and blame assignment for higher-order session types
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2016-10-24 | Paper |
Linear logic propositions as session types
Mathematical Structures in Computer Science | 2016-07-28 | Paper |
Corecursion and non-divergence in session-typed processes
Trustworthy Global Computing | 2016-06-09 | Paper |
Tridirectional typechecking
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-11-11 | Paper |
A modal analysis of staged computation
Journal of the ACM | 2015-10-30 | Paper |
Polarized Substructural Session Types
Lecture Notes in Computer Science | 2015-10-01 | Paper |
Intersection types and computational effects
Proceedings of the fifth ACM SIGPLAN international conference on Functional programming | 2015-09-11 | Paper |
A type theory for memory allocation and data layout
Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-09-11 | Paper |
Intuitionistic Letcc via Labelled Deduction
Electronic Notes in Theoretical Computer Science | 2015-03-23 | Paper |
Linear logical relations and observational equivalences for session-based concurrency
Information and Computation | 2014-11-28 | Paper |
A linear logic programming language for concurrent programming over graph structures
Theory and Practice of Logic Programming | 2014-11-25 | Paper |
Subtyping and intersection types revisited
Proceedings of the 12th ACM SIGPLAN international conference on Functional programming | 2014-07-21 | Paper |
Specifying properties of concurrent computations in CLF
Electronic Notes in Theoretical Computer Science | 2014-01-10 | Paper |
| A bidirectional refinement type system for LF | 2014-01-10 | Paper |
Behavioral polymorphism and parametricity in session-based communication
Programming Languages and Systems | 2013-08-05 | Paper |
Higher-order processes, functions, and sessions: a monadic integration
Programming Languages and Systems | 2013-08-05 | Paper |
Logical approximation for program analysis
Higher-Order and Symbolic Computation | 2013-01-08 | Paper |
| Cut reduction in linear logic as asynchronous session-typed communication | 2012-11-22 | Paper |
Linear logical relations for session-based concurrency
Programming Languages and Systems | 2012-06-22 | Paper |
Functions as session-typed processes
Foundations of Software Science and Computational Structures | 2012-06-22 | Paper |
Proof-carrying code in a session-typed process calculus
Certified Programs and Proofs | 2011-11-22 | Paper |
| Church and Curry: combining intrinsic and extrinsic typing | 2011-03-30 | Paper |
| scientific article; zbMATH DE number 5872266 (Why is no real title available?) | 2011-03-30 | Paper |
Refinement types for logical frameworks and their interpretation as proof irrelevance
Logical Methods in Computer Science | 2010-12-20 | Paper |
Session types as intuitionistic linear propositions
CONCUR 2010 - Concurrency Theory | 2010-08-31 | Paper |
A coverage checking algorithm for LF
Lecture Notes in Computer Science | 2010-05-07 | Paper |
Optimizing higher-order pattern unification.
Lecture Notes in Computer Science | 2010-04-20 | Paper |
Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
Automated Deduction – CADE-22 | 2009-07-28 | Paper |
Refinement Types as Proof Irrelevance
Lecture Notes in Computer Science | 2009-07-07 | Paper |
A Logical Characterization of Forward and Backward Chaining in the Inverse Method
Automated Reasoning | 2009-03-12 | Paper |
Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
Logic for Programming, Artificial Intelligence, and Reasoning | 2009-01-27 | Paper |
Linear Logical Algorithms
Automata, Languages and Programming | 2008-08-19 | Paper |
A logical characterization of forward and backward chaining in the inverse method
Journal of Automated Reasoning | 2008-06-11 | Paper |
Computer Science Logic
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Automated Deduction – CADE-20
Lecture Notes in Computer Science | 2006-11-01 | Paper |
CONCUR 2005 – Concurrency Theory
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Staged computation with names and necessity
Journal of Functional Programming | 2005-11-28 | Paper |
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science | 2005-08-18 | Paper |
| scientific article; zbMATH DE number 2185713 (Why is no real title available?) | 2005-07-04 | Paper |
A monadic analysis of information flow security with mutable state
Journal of Functional Programming | 2005-05-03 | Paper |
| scientific article; zbMATH DE number 2110615 (Why is no real title available?) | 2004-10-26 | Paper |
| scientific article; zbMATH DE number 2080280 (Why is no real title available?) | 2004-08-04 | Paper |
A linear logical framework
Information and Computation | 2004-03-04 | Paper |
A Linear Spine Calculus
Journal Of Logic And Computation | 2004-01-28 | Paper |
| scientific article; zbMATH DE number 1966243 (Why is no real title available?) | 2003-08-18 | Paper |
| scientific article; zbMATH DE number 1956517 (Why is no real title available?) | 2003-07-30 | Paper |
Structural cut elimination. I: Intuitionistic and classical logic
Information and Computation | 2003-01-14 | Paper |
A judgmental reconstruction of modal logic
MSCS. Mathematical Structures in Computer Science | 2002-11-11 | Paper |
| Logical frameworks | 2002-08-27 | Paper |
Primitive recursion for higher-order abstract syntax
Theoretical Computer Science | 2002-03-03 | Paper |
| scientific article; zbMATH DE number 1497779 (Why is no real title available?) | 2001-03-06 | Paper |
Efficient resource management for linear logic proof search
Theoretical Computer Science | 2000-08-23 | Paper |
| scientific article; zbMATH DE number 1420794 (Why is no real title available?) | 2000-03-22 | Paper |
| scientific article; zbMATH DE number 1342286 (Why is no real title available?) | 1999-11-21 | Paper |
| scientific article; zbMATH DE number 1303348 (Why is no real title available?) | 1999-11-07 | Paper |
| scientific article; zbMATH DE number 1348473 (Why is no real title available?) | 1999-10-10 | Paper |
| scientific article; zbMATH DE number 1330453 (Why is no real title available?) | 1999-09-21 | Paper |
| scientific article; zbMATH DE number 1231700 (Why is no real title available?) | 1999-01-10 | Paper |
| scientific article; zbMATH DE number 1231474 (Why is no real title available?) | 1998-12-13 | Paper |
A module system for a programming language based on the LF logical framework
Journal Of Logic And Computation | 1998-07-28 | Paper |
On the unification problem for Cartesian closed categories
Journal of Symbolic Logic | 1997-01-01 | Paper |
TPS: A theorem-proving system for classical type theory
Journal of Automated Reasoning | 1996-11-25 | Paper |
| scientific article; zbMATH DE number 445160 (Why is no real title available?) | 1993-12-05 | Paper |
| scientific article; zbMATH DE number 65531 (Why is no real title available?) | 1992-09-27 | Paper |
Uniform proofs as a foundation for logic programming
Annals of Pure and Applied Logic | 1991-01-01 | Paper |
| scientific article; zbMATH DE number 4133471 (Why is no real title available?) | 1990-01-01 | Paper |
| scientific article; zbMATH DE number 4180832 (Why is no real title available?) | 1989-01-01 | Paper |
| scientific article; zbMATH DE number 4063061 (Why is no real title available?) | 1988-01-01 | Paper |
| scientific article; zbMATH DE number 3871342 (Why is no real title available?) | 1984-01-01 | Paper |
| scientific article; zbMATH DE number 3878393 (Why is no real title available?) | 1984-01-01 | Paper |
