Typed Lambda Calculi and Applications

- Mathematical Synthesis of Equational Deduction Systems

- A Pronominal Approach to Binding and Computation

- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance

- Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1

- Syntax for Free: Representing Syntax with Binding Using Parametricity

- On the Meaning of Logical Completeness

- Thick Subtrees, Games and Experiments

- Bounded Linear Logic, Revisited

- Partial Orders, Event Structures and Linear Strategies

- Existential Type Systems with No Types in Terms

- Initial Algebra Semantics for Cyclic Sharing Structures

- An Operational Account of Call-by-Value Minimal and Classical ?-Calculus in "Natural Deduction" Form

- Refinement Types as Proof Irrelevance

- Weak ?-Categories from Intensional Type Theory

- Relating Classical Realizability and Negative Translation for Existential Witness Extraction

- Session-Based Communication Optimisation for Higher-Order Mobile Processes

- The Cut-Elimination Theorem for Differential Nets with Promotion

- A Polymorphic Type System for the Lambda-Calculus with Constructors

- Kripke Semantics for Martin-Löf's Extensional Type Theory

- On the Values of Reducibility Candidates

- Lexicographic Path Induction

- Parametricity for Haskell with Imprecise Error Semantics

- Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic

- Algebraic Totality, towards Completeness

- A Logical Foundation for Environment Classifiers

- Inhabitation of Low-Rank Intersection Types

- Differential Linear Logic and Polarization

- Complexity of Gödel's T in ?-Formulation

- The Computational SLR: A Logic for Reasoning about Computational Indistinguishability