TLCA 2013 Accepted Papers

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


Last update 23 March 2013