@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}
}
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing