Thorsten Altenkirch
Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications
TLCA, 2015.
@proceedings{TLCA-2015,
address = "Warsaw, Poland",
editor = "Thorsten Altenkirch",
ee = "http://www.dagstuhl.de/dagpub/978-3-939897-87-3",
isbn = "978-3-939897-87-3",
publisher = "{Schloss Dagstuhl — Leibniz-Zentrum für Informatik}",
series = "{Leibniz International Proceedings in Informatics}",
title = "{Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications}",
volume = 38,
year = 2015,
}
Contents (23 items)
- TLCA-2015-AfshariHL #context-free grammar
- Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars (BA, SH, GEL), pp. 1–16.
- TLCA-2015-AhrensCS #type system
- Non-Wellfounded Trees in Homotopy Type Theory (BA, PC, RS), pp. 17–30.
- TLCA-2015-Assaf #π-calculus
- Conservativity of Embeddings in the λ π Calculus Modulo Rewriting (AA0), pp. 31–44.
- TLCA-2015-AtkeyGFRS #modelling #morphism #physics #polymorphism
- Models for Polymorphism over Physical Dimension (RA, NG, FNF, TR, SS), pp. 45–59.
- TLCA-2015-Bagnol #diagrams #equivalence #proving
- MALL Proof Equivalence is Logspace-Complete, via Binary Decision Diagrams (MB), pp. 60–75.
- TLCA-2015-BessaiDDCdR #composition #mixin #synthesis
- Mixin Composition Synthesis Based on Intersection Types (JB, AD, BD, TCC, Ud, JR), pp. 76–91.
- TLCA-2015-BezemCP #set
- Non-Constructivity in Kan Simplicial Sets (MB, TC, EP), pp. 92–106.
- TLCA-2015-BiernackiP #logic #type system
- Logical Relations for Coherence of Effect Subtyping (DB, PP), pp. 107–122.
- TLCA-2015-BucciarelliKR #calculus
- Observability for Pair Pattern Calculi (AB, DK, SRDR), pp. 123–137.
- TLCA-2015-CastellanCD #similarity
- Undecidability of Equality in the Free Locally Cartesian Closed Category (SC, PC, PD), pp. 138–152.
- TLCA-2015-EscardoX #consistency #nondeterminism
- The Inconsistency of a Brouwerian Continuity Principle with the Curry-Howard Interpretation (MHE, CX), pp. 153–164.
- TLCA-2015-Santo #calculus #exclamation
- Curry-Howard for Sequent Calculus at Last! (JES), pp. 165–179.
- TLCA-2015-FairweatherFST #dependent type
- Dependent Types for Nominal Terms with Atom Substitutions (EF, MF, NS, AT), pp. 180–195.
- TLCA-2015-Frey #specification
- Realizability Toposes from Specifications (JF), pp. 196–210.
- TLCA-2015-GuerrieriPR #call-by #standard #λ-calculus
- Standardization of a Call-By-Value λ-Calculus (GG, LP, SRDR), pp. 211–225.
- TLCA-2015-HirschowitzHT #type system
- Wild ω-Categories for the Homotopy Hypothesis in Type Theory (AH, TH, NT), pp. 226–240.
- TLCA-2015-HofmannM #analysis #multi #term rewriting
- Multivariate Amortised Resource Analysis for Term Rewrite Systems (MH, GM), pp. 241–256.
- TLCA-2015-JouannaudL #termination
- Termination of Dependently Typed Rewrite Rules (JPJ, JL), pp. 257–272.
- TLCA-2015-Pientka0 #recursion
- Well-Founded Recursion over Contextual Objects (BP, AA), pp. 273–287.
- TLCA-2015-Redmond #parametricity #polynomial #λ-calculus
- Polynomial Time in the Parametric λ Calculus (BFR), pp. 288–301.
- TLCA-2015-Riba #automaton
- Fibrations of Tree Automata (CR), pp. 302–316.
- TLCA-2015-Scherer #multi
- Multi-Focusing on Extensional Rewriting with Sums (GS), pp. 317–331.
- TLCA-2015-WangC #independence #type system
- A Proof-theoretic Characterization of Independence in Type Theory (YW, KC), pp. 332–346.
