International Conference on
Rewriting, Deduction, and Programming
June 29 to July 3, 2015
Warsaw, Poland

TLCA 2015 Accepted Papers

Marc Bagnol. MALL proof equivalence is Logspace-complete, via binary decision diagrams
Brian Redmond. Polynomial Time in the Parametric Lambda Calculus
Jean-Pierre Jouannaud and Jian-Qi Li. Termination of dependently typed rewrite rules
Bahareh Afshari, Stefan Hetzl and Graham Leigh. Herbrand disjunctions, cut elimination and context-free tree grammars
Martin Escardo and Chuangjie Xu. Inconsistency of Brouwer's continuity axioms with the Curry-Howard interpretation
Antonio Bucciarelli, Delia Kesner and Simona Ronchi Della Rocca. Observability for Pair Pattern Calculi
Robert Atkey, Neil Ghani, Fredrik Nordvall Forsberg, Timothy Revell and Sam Staton. Models for Polymorphism over Physical Dimensions
Marc Bezem, Thierry Coquand and Erik Parmann. Non-constructivity in Kan Simplicial Sets
Jan Bessai, Andrej Dudenhefner, Boris Duedder, Ugo De'Liguoro, Tzu-Chun Chen and Jakob Rehof. Mixin Composition Synthesis based on Intersection Types
Benedikt Ahrens, Paolo Capriotti and Régis Spadotti. Non-wellfounded trees in Homotopy Type Theory
Giulio Guerrieri, Luca Paolini and Simona Ronchi Della Rocca. Standardization of a call-by-value calculus
André Hirschowitz, Tom Hirschowitz and Nicolas Tabareau. Strict omega-categories for the homotopy hypothesis in type theory
Dariusz Biernacki and Piotr Polesiuk. Logical relations for coherence of effect subtyping
Simon Castellan, Pierre Clairambault and Peter Dybjer. Undecidability of Equality in the Free Locally Cartesian Closed Category
José Espírito Santo. Curry-Howard for sequent calculus at last!
Brigitte Pientka and Andreas Abel. Well-founded Recursion over Contextual Objects
Yuting Wang and Kaustuv Chaudhuri. A proof-theoretic characterization of independence in type theory
Gabriel Scherer. Multi-focusing on extensional rewriting with sums
Elliot Fairweather, Maribel Fernandez, Nora Szasz and Alvaro Tasistro. Dependent Types for Nominal Terms with Atom Substitutions
Ali Assaf. Conservativity of embeddings in the lambda-Pi calculus modulo rewriting
Jonas Frey. Realizability toposes from specifications
Martin Hofmann and Georg Moser. Multivariate Amortised Resource Analysis for Term Rewrite Systems
Colin Riba. Fibrations of Tree Automata

Important information

Plenary speakers

Valid XHTML 1.1 Valid CSS!