13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@Proceedings{altenkirch:LIPIcs.TLCA.2015, title = {{LIPIcs, Volume 38, TLCA'15, Complete Volume}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015}, URN = {urn:nbn:de:0030-drops-52636}, doi = {10.4230/LIPIcs.TLCA.2015}, annote = {Keywords: Applicative (Functional) Programming, Language Classifications, Language Constructs and Features, Data Structures, Logics and Meanings of Programs Mathematical Logic and Formal Languages, Symbolic and Algebraic Manipulation, Deduction and Theorem Proving} }
13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. i-xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{altenkirch:LIPIcs.TLCA.2015.i, author = {Altenkirch, Thorsten}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {i--xii}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.i}, URN = {urn:nbn:de:0030-drops-51509}, doi = {10.4230/LIPIcs.TLCA.2015.i}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Bahareh Afshari, Stefan Hetzl, and Graham E. Leigh. Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{afshari_et_al:LIPIcs.TLCA.2015.1, author = {Afshari, Bahareh and Hetzl, Stefan and Leigh, Graham E.}, title = {{Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {1--16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.1}, URN = {urn:nbn:de:0030-drops-51516}, doi = {10.4230/LIPIcs.TLCA.2015.1}, annote = {Keywords: Classical logic, Context-free grammars, Cut elimination, First-order logic, Herbrand's theorem, Proof theory} }
Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-Wellfounded Trees in Homotopy Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 17-30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{ahrens_et_al:LIPIcs.TLCA.2015.17, author = {Ahrens, Benedikt and Capriotti, Paolo and Spadotti, R\'{e}gis}, title = {{Non-Wellfounded Trees in Homotopy Type Theory}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {17--30}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.17}, URN = {urn:nbn:de:0030-drops-51522}, doi = {10.4230/LIPIcs.TLCA.2015.17}, annote = {Keywords: Homotopy Type Theory, coinductive types, computer theorem proving, Agda} }
Ali Assaf. Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 31-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{assaf:LIPIcs.TLCA.2015.31, author = {Assaf, Ali}, title = {{Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {31--44}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.31}, URN = {urn:nbn:de:0030-drops-51535}, doi = {10.4230/LIPIcs.TLCA.2015.31}, annote = {Keywords: lambda Pi calculus modulo rewriting, pure type systems, logical framework, normalization, conservativit} }
Robert Atkey, Neil Ghani, Fredrik Nordvall Forsberg, Timothy Revell, and Sam Staton. Models for Polymorphism over Physical Dimension. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 45-59, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{atkey_et_al:LIPIcs.TLCA.2015.45, author = {Atkey, Robert and Ghani, Neil and Nordvall Forsberg, Fredrik and Revell, Timothy and Staton, Sam}, title = {{Models for Polymorphism over Physical Dimension}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {45--59}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.45}, URN = {urn:nbn:de:0030-drops-51547}, doi = {10.4230/LIPIcs.TLCA.2015.45}, annote = {Keywords: Category Theory, Units of Measure, Dimension Types, Type Theory} }
Marc Bagnol. MALL Proof Equivalence is Logspace-Complete, via Binary Decision Diagrams. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 60-75, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{bagnol:LIPIcs.TLCA.2015.60, author = {Bagnol, Marc}, title = {{MALL Proof Equivalence is Logspace-Complete, via Binary Decision Diagrams}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {60--75}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.60}, URN = {urn:nbn:de:0030-drops-51558}, doi = {10.4230/LIPIcs.TLCA.2015.60}, annote = {Keywords: linear logic, proof equivalence, additive connectives, proofnets, binary decision diagrams, logarithmic space, AC0 reductions} }
Jan Bessai, Andrej Dudenhefner, Boris Düdder, Tzu-Chun Chen, Ugo de’Liguoro, and Jakob Rehof. Mixin Composition Synthesis Based on Intersection Types. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 76-91, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{bessai_et_al:LIPIcs.TLCA.2015.76, author = {Bessai, Jan and Dudenhefner, Andrej and D\"{u}dder, Boris and Chen, Tzu-Chun and de’Liguoro, Ugo and Rehof, Jakob}, title = {{Mixin Composition Synthesis Based on Intersection Types}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {76--91}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.76}, URN = {urn:nbn:de:0030-drops-51563}, doi = {10.4230/LIPIcs.TLCA.2015.76}, annote = {Keywords: Record Calculus, Combinatory Logic, Type Inhabitation, Mixin, Intersection Type} }
Marc Bezem, Thierry Coquand, and Erik Parmann. Non-Constructivity in Kan Simplicial Sets. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 92-106, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{bezem_et_al:LIPIcs.TLCA.2015.92, author = {Bezem, Marc and Coquand, Thierry and Parmann, Erik}, title = {{Non-Constructivity in Kan Simplicial Sets}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {92--106}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.92}, URN = {urn:nbn:de:0030-drops-51579}, doi = {10.4230/LIPIcs.TLCA.2015.92}, annote = {Keywords: Constructive logic, simplicial sets, semantics of simple types} }
Dariusz Biernacki and Piotr Polesiuk. Logical Relations for Coherence of Effect Subtyping. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 107-122, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{biernacki_et_al:LIPIcs.TLCA.2015.107, author = {Biernacki, Dariusz and Polesiuk, Piotr}, title = {{Logical Relations for Coherence of Effect Subtyping}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {107--122}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.107}, URN = {urn:nbn:de:0030-drops-51580}, doi = {10.4230/LIPIcs.TLCA.2015.107}, annote = {Keywords: type system, coherence of subtyping, logical relation, control effect, continuation-passing style} }
Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Observability for Pair Pattern Calculi. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 123-137, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{bucciarelli_et_al:LIPIcs.TLCA.2015.123, author = {Bucciarelli, Antonio and Kesner, Delia and Ronchi Della Rocca, Simona}, title = {{Observability for Pair Pattern Calculi}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {123--137}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.123}, URN = {urn:nbn:de:0030-drops-51596}, doi = {10.4230/LIPIcs.TLCA.2015.123}, annote = {Keywords: solvability, pattern calculi, intersection types, inhabitation} }
Simon Castellan, Pierre Clairambault, and Peter Dybjer. Undecidability of Equality in the Free Locally Cartesian Closed Category. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 138-152, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{castellan_et_al:LIPIcs.TLCA.2015.138, author = {Castellan, Simon and Clairambault, Pierre and Dybjer, Peter}, title = {{Undecidability of Equality in the Free Locally Cartesian Closed Category}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {138--152}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.138}, URN = {urn:nbn:de:0030-drops-51602}, doi = {10.4230/LIPIcs.TLCA.2015.138}, annote = {Keywords: Extensional type theory, locally cartesian closed categories, undecidab- ility} }
Martín Hötzel Escardó and Chuangjie Xu. The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 153-164, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{hotzelescardo_et_al:LIPIcs.TLCA.2015.153, author = {H\"{o}tzel Escard\'{o}, Mart{\'\i}n and Xu, Chuangjie}, title = {{The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {153--164}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.153}, URN = {urn:nbn:de:0030-drops-51618}, doi = {10.4230/LIPIcs.TLCA.2015.153}, annote = {Keywords: Dependent type, intensional Martin-L\"{o}f type theory, Curry-Howard interpretation, constructive mathematics, Brouwerian continuity axioms, anonymous exi} }
José Espírito Santo. Curry-Howard for Sequent Calculus at Last!. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 165-179, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{espiritosanto:LIPIcs.TLCA.2015.165, author = {Esp{\'\i}rito Santo, Jos\'{e}}, title = {{Curry-Howard for Sequent Calculus at Last!}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {165--179}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.165}, URN = {urn:nbn:de:0030-drops-51626}, doi = {10.4230/LIPIcs.TLCA.2015.165}, annote = {Keywords: co-control, co-continuation, vector notation, let-expression, formal sub- stitution, context substitution, computational lambda-calculus, classical lo} }
Elliot Fairweather, Maribel Fernández, Nora Szasz, and Alvaro Tasistro. Dependent Types for Nominal Terms with Atom Substitutions. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 180-195, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{fairweather_et_al:LIPIcs.TLCA.2015.180, author = {Fairweather, Elliot and Fern\'{a}ndez, Maribel and Szasz, Nora and Tasistro, Alvaro}, title = {{Dependent Types for Nominal Terms with Atom Substitutions}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {180--195}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.180}, URN = {urn:nbn:de:0030-drops-51636}, doi = {10.4230/LIPIcs.TLCA.2015.180}, annote = {Keywords: alpha-equivalence, nominal term, substitution, dependent type} }
Jonas Frey. Realizability Toposes from Specifications. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 196-210, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{frey:LIPIcs.TLCA.2015.196, author = {Frey, Jonas}, title = {{Realizability Toposes from Specifications}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {196--210}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.196}, URN = {urn:nbn:de:0030-drops-51645}, doi = {10.4230/LIPIcs.TLCA.2015.196}, annote = {Keywords: Krivine machine, classical realizability, realizability topos, bisimulation} }
Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca. Standardization of a Call-By-Value Lambda-Calculus. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 211-225, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{guerrieri_et_al:LIPIcs.TLCA.2015.211, author = {Guerrieri, Giulio and Paolini, Luca and Ronchi Della Rocca, Simona}, title = {{Standardization of a Call-By-Value Lambda-Calculus}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {211--225}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.211}, URN = {urn:nbn:de:0030-drops-51655}, doi = {10.4230/LIPIcs.TLCA.2015.211}, annote = {Keywords: standardization,sequentialization,lambda-calculus,sigma-reduction,par- allel reduction, call-by-value, head reduction, internal reduction, solvability} }
André Hirschowitz, Tom Hirschowitz, and Nicolas Tabareau. Wild omega-Categories for the Homotopy Hypothesis in Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 226-240, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{hirschowitz_et_al:LIPIcs.TLCA.2015.226, author = {Hirschowitz, Andr\'{e} and Hirschowitz, Tom and Tabareau, Nicolas}, title = {{Wild omega-Categories for the Homotopy Hypothesis in Type Theory}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {226--240}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.226}, URN = {urn:nbn:de:0030-drops-51669}, doi = {10.4230/LIPIcs.TLCA.2015.226}, annote = {Keywords: Homotopy Type theory; Omega-categories; Coinduction; Homotopy hypothesis} }
Martin Hofmann and Georg Moser. Multivariate Amortised Resource Analysis for Term Rewrite Systems. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 241-256, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{hofmann_et_al:LIPIcs.TLCA.2015.241, author = {Hofmann, Martin and Moser, Georg}, title = {{Multivariate Amortised Resource Analysis for Term Rewrite Systems}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {241--256}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.241}, URN = {urn:nbn:de:0030-drops-51675}, doi = {10.4230/LIPIcs.TLCA.2015.241}, annote = {Keywords: program analysis,amortised analysis, term rewriting,multivariate bounds} }
Jean-Pierre Jouannaud and Jianqi Li. Termination of Dependently Typed Rewrite Rules. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 257-272, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{jouannaud_et_al:LIPIcs.TLCA.2015.257, author = {Jouannaud, Jean-Pierre and Li, Jianqi}, title = {{Termination of Dependently Typed Rewrite Rules}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {257--272}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.257}, URN = {urn:nbn:de:0030-drops-51684}, doi = {10.4230/LIPIcs.TLCA.2015.257}, annote = {Keywords: rewriting, dependent types, strong normalization, path orderings} }
Brigitte Pientka and Andreas Abel. Well-Founded Recursion over Contextual Objects. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 273-287, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{pientka_et_al:LIPIcs.TLCA.2015.273, author = {Pientka, Brigitte and Abel, Andreas}, title = {{Well-Founded Recursion over Contextual Objects}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {273--287}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.273}, URN = {urn:nbn:de:0030-drops-51699}, doi = {10.4230/LIPIcs.TLCA.2015.273}, annote = {Keywords: Type systems, Dependent Types, Logical Frameworks} }
Brian F. Redmond. Polynomial Time in the Parametric Lambda Calculus. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 288-301, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{redmond:LIPIcs.TLCA.2015.288, author = {Redmond, Brian F.}, title = {{Polynomial Time in the Parametric Lambda Calculus}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {288--301}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.288}, URN = {urn:nbn:de:0030-drops-51705}, doi = {10.4230/LIPIcs.TLCA.2015.288}, annote = {Keywords: Parametric Lambda Calculus, Polynomial Time Complexity, Combinators, Nondeterminism and Explicit Products, Implicit Computational Complexity} }
Colin Riba. Fibrations of Tree Automata. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 302-316, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{riba:LIPIcs.TLCA.2015.302, author = {Riba, Colin}, title = {{Fibrations of Tree Automata}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {302--316}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.302}, URN = {urn:nbn:de:0030-drops-51719}, doi = {10.4230/LIPIcs.TLCA.2015.302}, annote = {Keywords: Tree automata, Game semantics, Categorical logic.} }
Gabriel Scherer. Multi-Focusing on Extensional Rewriting with Sums. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 317-331, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{scherer:LIPIcs.TLCA.2015.317, author = {Scherer, Gabriel}, title = {{Multi-Focusing on Extensional Rewriting with Sums}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {317--331}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.317}, URN = {urn:nbn:de:0030-drops-51721}, doi = {10.4230/LIPIcs.TLCA.2015.317}, annote = {Keywords: Maximal multi-focusing, extensional sums, rewriting, natural deduction} }
Yuting Wang and Kaustuv Chaudhuri. A Proof-theoretic Characterization of Independence in Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 332-346, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{wang_et_al:LIPIcs.TLCA.2015.332, author = {Wang, Yuting and Chaudhuri, Kaustuv}, title = {{A Proof-theoretic Characterization of Independence in Type Theory}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {332--346}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.332}, URN = {urn:nbn:de:0030-drops-51736}, doi = {10.4230/LIPIcs.TLCA.2015.332}, annote = {Keywords: subordination; independence; sequent calculus; focusing; strengthening} }
Feedback for Dagstuhl Publishing