| Publication | Date of Publication | Type |
|---|
| Type-based termination for futures | 2024-05-27 | Paper |
| Manifest deadlock-freedom for shared session types | 2023-11-24 | Paper |
| A logical framework with higher-order rational (circular) terms | 2023-11-24 | Paper |
| Polarized subtyping | 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 | 2023-04-12 | Paper |
| The practice of logical frameworks | 2023-02-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5875401 | 2023-02-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5094136 | 2022-08-02 | Paper |
| Session Types with Arithmetic Refinements | 2022-07-18 | Paper |
| Back to futures | 2022-03-17 | Paper |
| A Linear Logic of Authorization and Knowledge | 2022-03-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5028463 | 2022-02-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5014814 | 2021-12-08 | Paper |
| Session-typed concurrent contracts | 2021-11-24 | Paper |
| Nested session types | 2021-10-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5009447 | 2021-08-04 | Paper |
| A message-passing interpretation of adjoint logic | 2021-06-25 | Paper |
| Work Analysis with Resource-Aware Session Types | 2021-01-20 | Paper |
| Elf: A meta-language for deductive systems | 2020-01-21 | Paper |
| Session-typed concurrent contracts | 2019-09-13 | Paper |
| A probabilistic language based upon sampling functions | 2017-07-14 | Paper |
| Contextual modal type theory | 2017-07-12 | Paper |
| On equivalence and canonical forms in the LF type theory | 2017-07-12 | Paper |
| Higher-order pattern complement and the strict λ-calculus | 2017-06-13 | Paper |
| Substructural Proofs as Automata | 2016-12-21 | Paper |
| Monitors and blame assignment for higher-order session types | 2016-10-24 | Paper |
| Linear logic propositions as session types | 2016-07-28 | Paper |
| Corecursion and Non-divergence in Session-Typed Processes | 2016-06-09 | Paper |
| Tridirectional typechecking | 2015-11-11 | Paper |
| A modal analysis of staged computation | 2015-10-30 | Paper |
| Polarized Substructural Session Types | 2015-10-01 | Paper |
| Intersection types and computational effects | 2015-09-11 | Paper |
| A type theory for memory allocation and data layout | 2015-09-11 | Paper |
| Intuitionistic Letcc via Labelled Deduction | 2015-03-23 | Paper |
| Linear logical relations and observational equivalences for session-based concurrency | 2014-11-28 | Paper |
| A Linear Logic Programming Language for Concurrent Programming over Graph Structures | 2014-11-25 | Paper |
| Subtyping and intersection types revisited | 2014-07-21 | Paper |
| Specifying properties of concurrent computations in CLF | 2014-01-10 | Paper |
| A bidirectional refinement type system for LF | 2014-01-10 | Paper |
| Behavioral Polymorphism and Parametricity in Session-Based Communication | 2013-08-05 | Paper |
| Higher-Order Processes, Functions, and Sessions: A Monadic Integration | 2013-08-05 | Paper |
| Logical approximation for program analysis | 2013-01-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4649549 | 2012-11-22 | Paper |
| Linear Logical Relations for Session-Based Concurrency | 2012-06-22 | Paper |
| Functions as Session-Typed Processes | 2012-06-22 | Paper |
| Proof-Carrying Code in a Session-Typed Process Calculus | 2011-11-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3086784 | 2011-03-30 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3086786 | 2011-03-30 | Paper |
| Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance | 2010-12-20 | Paper |
| Session Types as Intuitionistic Linear Propositions | 2010-08-31 | Paper |
| A Coverage Checking Algorithm for LF | 2010-05-07 | Paper |
| Automated Deduction – CADE-19 | 2010-04-20 | Paper |
| Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method | 2009-07-28 | Paper |
| Refinement Types as Proof Irrelevance | 2009-07-07 | Paper |
| A Logical Characterization of Forward and Backward Chaining in the Inverse Method | 2009-03-12 | Paper |
| Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic | 2009-01-27 | Paper |
| Linear Logical Algorithms | 2008-08-19 | Paper |
| A logical characterization of forward and backward chaining in the inverse method | 2008-06-11 | Paper |
| Computer Science Logic | 2006-11-01 | Paper |
| Automated Deduction – CADE-20 | 2006-11-01 | Paper |
| CONCUR 2005 – Concurrency Theory | 2006-11-01 | Paper |
| Staged computation with names and necessity | 2005-11-28 | Paper |
| Theorem Proving in Higher Order Logics | 2005-08-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3024905 | 2005-07-04 | Paper |
| A monadic analysis of information flow security with mutable state | 2005-05-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4823135 | 2004-10-26 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4472531 | 2004-08-04 | Paper |
| A linear logical framework | 2004-03-04 | Paper |
| A Linear Spine Calculus | 2004-01-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4420573 | 2003-08-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4417863 | 2003-07-30 | Paper |
| Structural cut elimination. I: Intuitionistic and classical logic | 2003-01-14 | Paper |
| A judgmental reconstruction of modal logic | 2002-11-11 | Paper |
| Logical frameworks | 2002-08-27 | Paper |
| Primitive recursion for higher-order abstract syntax | 2002-03-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4499196 | 2001-03-06 | Paper |
| Efficient resource management for linear logic proof search | 2000-08-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4944858 | 2000-03-22 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4263877 | 1999-11-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4249901 | 1999-11-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4264727 | 1999-10-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4261096 | 1999-09-21 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4223031 | 1999-01-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4222777 | 1998-12-13 | Paper |
| A module system for a programming language based on the LF logical framework | 1998-07-28 | Paper |
| On the unification problem for Cartesian closed categories | 1997-01-01 | Paper |
| TPS: A theorem-proving system for classical type theory | 1996-11-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3142167 | 1993-12-05 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4012879 | 1992-09-27 | Paper |
| Uniform proofs as a foundation for logic programming | 1991-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3034803 | 1990-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3204068 | 1989-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3797157 | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3338233 | 1984-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3343471 | 1984-01-01 | Paper |
