Ki Yung Ahn, Tim Sheard, Marcelo Fiore and Andrew Pitts.
System Fi: a Higher-Order Polymorphic Lambda Calculus with Erasable Term-Indices
Federico Aschieri and Margherita Zorzi.
Non-Determinism and the Strong Normalization of System T
Nick Benton, Martin Hofmann and Vivek Nigam.
Proof-Relevant Logical Relations for Name Generation
Stefano Berardi and Makoto Tatsuta.
Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics
Valentin Blot.
Realizability for Peano Arithmetic with Winning Conditions in HO Games
Flavien Breuvart.
The Resource Lambda Calculus is Short-sighted in Its Relational Model
Pierre Clairambault.
Bounding Skeletons, Locally Scoped Terms and Exact Bounds for Linear Head Reduction
Boris Düdder, Moritz Martens and Jakob Rehof.
Intersection Type Matching with Subtyping
Martin Escardo and Chuangjie Xu.
A Constructive Model of Uniform Continuity
Daniel Fridlender and Miguel Pagano.
A Type-checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation
Neil Ghani, Peter Hancock, Lorenzo Malatesta, Conor McBride and Thorsten Altenkirch.
Small Induction Recursion
Nicolai Kraus, Martin Escardo, Thierry Coquand and Thorsten Altenkirch.
Generalizations of Hedberg's Theorem
Sylvain Salvati and Igor Walukiewicz.
Using Models to Model-Check Recursive Schemes
Ulrich Schöpp.
On Interaction, Continuations and Defunctionalization
Paula Severi and Fer-Jan de Vries.
Completeness of Conversion between Reactive Programs for Ultrametric Models
Home TLCA 2013 | Call for Papers | Accepted Papers | Invited Speakers | Organizers
Home RDP 2013 | Call for Workshops for RDP 2013 | Organizing Committee of RDP 2013