@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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.}
}
@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}
}
@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}
}