Typed Lambda Calculi and Applications - researchr conference series publications

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 100 from 321

2015

Multivariate Amortised Resource Analysis for Term Rewrite SystemsMartin Hofmann 0001, Georg Moser. tlca 2015: 241-256 [doi]

Front Matter, Table of Contents, Preface, Conference Organizationtlca 2015: [doi]

Herbrand Disjunctions, Cut Elimination and Context-Free Tree GrammarsBahareh Afshari, Stefan Hetzl, Graham Emil Leigh. tlca 2015: 1-16 [doi]

Non-Wellfounded Trees in Homotopy Type TheoryBenedikt Ahrens, Paolo Capriotti, Régis Spadotti. tlca 2015: 17-30 [doi]

13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, PolandThorsten Altenkirch, editor, Volume 38 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. [doi]

Conservativity of Embeddings in the lambda Pi Calculus Modulo RewritingAli Assaf. tlca 2015: 31-44 [doi]

Models for Polymorphism over Physical DimensionRobert Atkey, Neil Ghani, Fredrik Nordvall Forsberg, Timothy Revell, Sam Staton. tlca 2015: 45-59 [doi]

MALL Proof Equivalence is Logspace-Complete, via Binary Decision DiagramsMarc Bagnol. tlca 2015: 60-75 [doi]

Mixin Composition Synthesis Based on Intersection TypesJan Bessai, Andrej Dudenhefner, Boris Düdder, Tzu-Chun Chen, Ugo de'Liguoro, Jakob Rehof. tlca 2015: 76-91 [doi]

Non-Constructivity in Kan Simplicial SetsMarc Bezem, Thierry Coquand, Erik Parmann. tlca 2015: 92-106 [doi]

Logical Relations for Coherence of Effect SubtypingDariusz Biernacki, Piotr Polesiuk. tlca 2015: 107-122 [doi]

Observability for Pair Pattern CalculiAntonio Bucciarelli, Delia Kesner, Simona Ronchi Della Rocca. tlca 2015: 123-137 [doi]

Undecidability of Equality in the Free Locally Cartesian Closed CategorySimon Castellan, Pierre Clairambault, Peter Dybjer. tlca 2015: 138-152 [doi]

The Inconsistency of a Brouwerian Continuity Principle with the Curry-Howard InterpretationMartín Hötzel Escardó, Chuangjie Xu. tlca 2015: 153-164 [doi]

Dependent Types for Nominal Terms with Atom SubstitutionsElliot Fairweather, Maribel Fernández, Nora Szasz, Alvaro Tasistro. tlca 2015: 180-195 [doi]

Realizability Toposes from SpecificationsJonas Frey. tlca 2015: 196-210 [doi]

Standardization of a Call-By-Value Lambda-CalculusGiulio Guerrieri, Luca Paolini, Simona Ronchi Della Rocca. tlca 2015: 211-225 [doi]

Wild omega-Categories for the Homotopy Hypothesis in Type TheoryAndré Hirschowitz, Tom Hirschowitz, Nicolas Tabareau. tlca 2015: 226-240 [doi]

Termination of Dependently Typed Rewrite RulesJean-Pierre Jouannaud, Jianqi Li. tlca 2015: 257-272 [doi]

Well-Founded Recursion over Contextual ObjectsBrigitte Pientka, Andreas Abel 0001. tlca 2015: 273-287 [doi]

Polynomial Time in the Parametric Lambda CalculusBrian F. Redmond. tlca 2015: 288-301 [doi]

Fibrations of Tree AutomataColin Riba. tlca 2015: 302-316 [doi]

Curry-Howard for Sequent Calculus at Last!José Espírito Santo. tlca 2015: 165-179 [doi]

Multi-Focusing on Extensional Rewriting with SumsGabriel Scherer. tlca 2015: 317-331 [doi]

A Proof-theoretic Characterization of Independence in Type TheoryYuTing Wang, Kaustuv Chaudhuri. tlca 2015: 332-346 [doi]

2013

i Ki Yung Ahn, Tim Sheard, Marcelo P. Fiore, Andrew M. Pitts. tlca 2013: 15-30 [doi]

Non-determinism, Non-termination and the Strong Normalization of System TFederico Aschieri, Margherita Zorzi. tlca 2013: 31-47 [doi]

Proof-Relevant Logical Relations for Name GenerationNick Benton, Martin Hofmann, Vivek Nigam. tlca 2013: 48-60 [doi]

Games with Sequential Backtracking and Complete Game Semantics for Subclassical LogicsStefano Berardi, Makoto Tatsuta. tlca 2013: 61-76 [doi]

Realizability for Peano Arithmetic with Winning Conditions in HON GamesValentin Blot. tlca 2013: 77-92 [doi]

The Resource Lambda Calculus Is Short-Sighted in Its Relational ModelFlavien Breuvart. tlca 2013: 93-108 [doi]

Bounding Skeletons, Locally Scoped Terms and Exact Bounds for Linear Head ReductionPierre Clairambault. tlca 2013: 109-124 [doi]

Intersection Type Matching with SubtypingBoris Düdder, Moritz Martens, Jakob Rehof. tlca 2013: 125-139 [doi]

A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by EvaluationDaniel Fridlender, Miguel Pagano. tlca 2013: 140-155 [doi]

Small Induction RecursionPeter Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta, Thorsten Altenkirch. tlca 2013: 156-172 [doi]

Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. ProceedingsMasahito Hasegawa, editor, Volume 7941 of Lecture Notes in Computer Science, Springer, 2013. [doi]

Proving with Side EffectsHugo Herbelin. tlca 2013: 2 [doi]

Generalizations of Hedberg's TheoremNicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, Thorsten Altenkirch. tlca 2013: 173-188 [doi]

Non-linearity as the Metric Completion of LinearityDamiano Mazza. tlca 2013: 3-14 [doi]

Type-Directed Compilation in the Wild: Haskell and CoreSimon L. Peyton Jones. tlca 2013: 1 [doi]

Using Models to Model-Check Recursive SchemesSylvain Salvati, Igor Walukiewicz. tlca 2013: 189-204 [doi]

On Interaction, Continuations and DefunctionalizationUlrich Schöpp. tlca 2013: 205-220 [doi]

Completeness of Conversion between Reactive Programs for Ultrametric ModelsPaula Severi, Fer-Jan de Vries. tlca 2013: 221-235 [doi]

A Constructive Model of Uniform ContinuityChuangjie Xu, Martín Hötzel Escardó. tlca 2013: 236-249 [doi]

2011

Higher-Order Dynamic Pattern Unification for Dependent Types and RecordsAndreas Abel, Brigitte Pientka. tlca 2011: 10-26 [doi]

Classical Call-by-Need and DualityZena M. Ariola, Hugo Herbelin, Alexis Saurin. tlca 2011: 27-44 [doi]

Homotopy-Theoretic Models of Type TheoryPeter Arndt, Krzysztof Kapulkin. tlca 2011: 45-60 [doi]

Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed ::::λ::::-CalculusPierre Bourreau, Sylvain Salvati. tlca 2011: 61-75 [doi]

Orthogonality and Boolean Algebras for Deduction ModuloAloïs Brunel, Olivier Hermant, Clément Houtmann. tlca 2011: 76-90 [doi]

The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type TheoriesPierre Clairambault, Peter Dybjer. tlca 2011: 91-106 [doi]

Realizability Proof for Normalization of Full Differential Linear LogicStéphane Gimenez. tlca 2011: 107-122 [doi]

Controlling Program Extraction in Light LogicsMarc Lasson. tlca 2011: 123-137 [doi]

An Elementary Affine ::::λ::::-Calculus with Multithreading and Side EffectsAntoine Madet, Roberto M. Amadio. tlca 2011: 138-152 [doi]

Böhm s Theorem for Resource Lambda Calculus through Taylor ExpansionGiulio Manzonetto, Michele Pagani. tlca 2011: 153-168 [doi]

A Survey of Classical RealizabilityAlexandre Miquel. tlca 2011: 1-2 [doi]

Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. ProceedingsC.-H. Luke Ong, editor, Volume 6690 of Lecture Notes in Computer Science, Springer, 2011. [doi]

Finite Combinatory Logic with Intersection TypesJakob Rehof, Pawel Urzyczyn. tlca 2011: 169-183 [doi]

Linear Lambda Calculus and Deep InferenceLuca Roversi. tlca 2011: 184-197 [doi]

Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming - (Extended Abstract)Reuben Rowe, Steffen van Bakel. tlca 2011: 229-244 [doi]

Partiality, State and Dependent TypesKasper Svendsen, Lars Birkedal, Aleksandar Nanevski. tlca 2011: 198-212 [doi]

Tree Automata, (Dis-)Equality Constraints and Term Rewriting - What s New?Sophie Tison. tlca 2011: 3-5 [doi]

Rewriting in PracticeAshish Tiwari. tlca 2011: 6-8 [doi]

A Filter Model for the ::::λμ::::-Calculus - (Extended Abstract)Steffen van Bakel, Franco Barbanera, Ugo de Liguoro. tlca 2011: 213-228 [doi]

Combining Proofs and ProgramsStephanie Weirich. tlca 2011: 9 [doi]

2009

A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof IrrelevanceAndreas Abel, Thierry Coquand, Miguel Pagano. tlca 2009: 5-19 [doi]

Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1Federico Aschieri, Stefano Berardi. tlca 2009: 20-34 [doi]

Syntax for Free: Representing Syntax with Binding Using ParametricityRobert Atkey. tlca 2009: 35-49 [doi]

Kripke Semantics for Martin-LÃ¶f s Extensional Type TheorySteven Awodey, Florian Rabe. tlca 2009: 249-263 [doi]

On the Meaning of Logical CompletenessMichele Basaldella, Kazushige Terui. tlca 2009: 50-64 [doi]

Thick Subtrees, Games and ExperimentsPierre Boudes. tlca 2009: 65-79 [doi]

Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. ProceedingsPierre-Louis Curien, editor, Volume 5608 of Lecture Notes in Computer Science, Springer, 2009. [doi]

Partial Orders, Event Structures and Linear StrategiesClaudia Faggian, Mauro Piccolo. tlca 2009: 95-111 [doi]

Mathematical Synthesis of Equational Deduction SystemsMarcelo P. Fiore, Chung-Kil Hur. tlca 2009: 1-2 [doi]

Existential Type Systems with No Types in TermsKen-etsu Fujita, Aleksy Schubert. tlca 2009: 112-126 [doi]

Initial Algebra Semantics for Cyclic Sharing StructuresMakoto Hamana. tlca 2009: 127-141 [doi]

A Pronominal Approach to Binding and ComputationRobert Harper, Daniel R. Licata, Noam Zeilberger. tlca 2009: 3-4 [doi]

An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in Natural Deduction FormHugo Herbelin, StÃ©phane Zimmermann. tlca 2009: 142-156 [doi]

Bounded Linear Logic, RevisitedUgo Dal Lago, Martin Hofmann. tlca 2009: 80-94 [doi]

Refinement Types as Proof IrrelevanceWilliam Lovas, Frank Pfenning. tlca 2009: 157-171 [doi]

Weak omega-Categories from Intensional Type TheoryPeter LeFanu Lumsdaine. tlca 2009: 172-187 [doi]

Relating Classical Realizability and Negative Translation for Existential Witness ExtractionAlexandre Miquel. tlca 2009: 188-202 [doi]

Session-Based Communication Optimisation for Higher-Order Mobile ProcessesDimitris Mostrous, Nobuko Yoshida. tlca 2009: 203-218 [doi]

The Cut-Elimination Theorem for Differential Nets with PromotionMichele Pagani. tlca 2009: 219-233 [doi]

A Polymorphic Type System for the Lambda-Calculus with ConstructorsBarbara Petit. tlca 2009: 234-248 [doi]

On the Values of Reducibility CandidatesColin Riba. tlca 2009: 264-278 [doi]

Lexicographic Path InductionJeffrey Sarnat, Carsten SchÃ¼rmann. tlca 2009: 279-293 [doi]

Parametricity for Haskell with Imprecise Error SemanticsFlorian Stenger, Janis Voigtländer. tlca 2009: 294-308 [doi]

Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear LogicLutz StraÃŸburger. tlca 2009: 309-324 [doi]

Algebraic Totality, towards CompletenessChristine Tasson. tlca 2009: 325-340 [doi]

A Logical Foundation for Environment ClassifiersTakeshi Tsukada, Atsushi Igarashi. tlca 2009: 341-355 [doi]

Inhabitation of Low-Rank Intersection TypesPawel Urzyczyn. tlca 2009: 356-370 [doi]

Differential Linear Logic and PolarizationLionel Vaux. tlca 2009: 371-385 [doi]

Complexity of GÃ¶del s T in lambda-FormulationGunnar Wilken, Andreas Weiermann. tlca 2009: 386-400 [doi]

The Computational SLR: A Logic for Reasoning about Computational IndistinguishabilityYu Zhang. tlca 2009: 401-415 [doi]

Links

Filter by Year
OR AND NOT 1

Filter by Tag

[+]
OR AND NOT 1

Filter by Author

[+]
OR AND NOT 1

Filter by Top terms

[+]
OR AND NOT 1

Typed Lambda Calculi and Applications (tlca)

Viewing Publication 1 - 100 from 321

2015

2013

2011

2009

2007

Links

Filter by YearOR AND NOT 1

Filter by Tag [+]OR AND NOT 1

Filter by Author [+]OR AND NOT 1

Filter by Top terms [+]OR AND NOT 1

Typed Lambda Calculi and Applications (tlca)

Viewing Publication 1 - 100 from 321

2015

2013

2011

2009

2007

Filter by Year
OR AND NOT 1

Filter by Tag

[+]
OR AND NOT 1

Filter by Author

[+]
OR AND NOT 1

Filter by Top terms

[+]
OR AND NOT 1