| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Jonas Frey |
Realizability Toposes from Specifications.  |
TLCA  |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Yuting Wang 0001, Kaustuv Chaudhuri |
A Proof-theoretic Characterization of Independence in Type Theory. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon Castellan, Pierre Clairambault, Peter Dybjer |
Undecidability of Equality in the Free Locally Cartesian Closed Category. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Dariusz Biernacki, Piotr Polesiuk |
Logical Relations for Coherence of Effect Subtyping. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Ali Assaf 0002 |
Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Gabriel Scherer |
Multi-Focusing on Extensional Rewriting with Sums. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Brian F. Redmond |
Polynomial Time in the Parametric Lambda Calculus. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | |
Front Matter, Table of Contents, Preface, Conference Organization. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Antonio Bucciarelli, Delia Kesner, Simona Ronchi Della Rocca |
Observability for Pair Pattern Calculi. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-Pierre Jouannaud, Jianqi Li |
Termination of Dependently Typed Rewrite Rules. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Giulio Guerrieri, Luca Paolini, Simona Ronchi Della Rocca |
Standardization of a Call-By-Value Lambda-Calculus. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin Hofmann 0001, Georg Moser |
Multivariate Amortised Resource Analysis for Term Rewrite Systems. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Atkey, Neil Ghani, Fredrik Nordvall Forsberg, Timothy Revell, Sam Staton |
Models for Polymorphism over Physical Dimension. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Marc Bezem, Thierry Coquand, Erik Parmann |
Non-Constructivity in Kan Simplicial Sets. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Benedikt Ahrens, Paolo Capriotti, Régis Spadotti |
Non-Wellfounded Trees in Homotopy Type Theory. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Elliot Fairweather, Maribel Fernández, Nora Szasz, Alvaro Tasistro |
Dependent Types for Nominal Terms with Atom Substitutions. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Thorsten Altenkirch (eds.) |
13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland |
TLCA |
2015 |
DBLP BibTeX RDF |
|
| 1 | Jan Bessai, Andrej Dudenhefner, Boris Düdder, Tzu-Chun Chen, Ugo de'Liguoro, Jakob Rehof |
Mixin Composition Synthesis Based on Intersection Types. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Brigitte Pientka, Andreas Abel 0001 |
Well-Founded Recursion over Contextual Objects. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | José Espírito Santo |
Curry-Howard for Sequent Calculus at Last!. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Bahareh Afshari, Stefan Hetzl, Graham Emil Leigh |
Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Martín Hötzel Escardó, Chuangjie Xu |
The Inconsistency of a Brouwerian Continuity Principle with the Curry-Howard Interpretation. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Marc Bagnol |
MALL Proof Equivalence is Logspace-Complete, via Binary Decision Diagrams. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Colin Riba |
Fibrations of Tree Automata. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | André Hirschowitz, Tom Hirschowitz, Nicolas Tabareau |
Wild omega-Categories for the Homotopy Hypothesis in Type Theory. |
TLCA |
2015 |
DBLP DOI BibTeX RDF |
|
| 1 | Flavien Breuvart |
The Resource Lambda Calculus Is Short-Sighted in Its Relational Model. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Damiano Mazza |
Non-linearity as the Metric Completion of Linearity. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter G. Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta, Thorsten Altenkirch |
Small Induction Recursion. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Pierre Clairambault |
Bounding Skeletons, Locally Scoped Terms and Exact Bounds for Linear Head Reduction. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Boris Düdder, Moritz Martens, Jakob Rehof |
Intersection Type Matching with Subtyping. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Simon L. Peyton Jones |
Type-Directed Compilation in the Wild: Haskell and Core. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Sylvain Salvati, Igor Walukiewicz |
Using Models to Model-Check Recursive Schemes. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Nicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, Thorsten Altenkirch |
Generalizations of Hedberg's Theorem. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Chuangjie Xu, Martín Hötzel Escardó |
A Constructive Model of Uniform Continuity. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Paula Severi, Fer-Jan de Vries |
Completeness of Conversion between Reactive Programs for Ultrametric Models. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefano Berardi, Makoto Tatsuta |
Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Ulrich Schöpp |
On Interaction, Continuations and Defunctionalization. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Nick Benton, Martin Hofmann 0001, Vivek Nigam |
Proof-Relevant Logical Relations for Name Generation. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Masahito Hasegawa (eds.) |
Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Hugo Herbelin |
Proving with Side Effects. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Fridlender, Miguel Pagano |
A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Ki Yung Ahn, Tim Sheard, Marcelo P. Fiore, Andrew M. Pitts |
System F i . |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Federico Aschieri, Margherita Zorzi |
Non-determinism, Non-termination and the Strong Normalization of System T. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Valentin Blot |
Realizability for Peano Arithmetic with Winning Conditions in HON Games. |
TLCA |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | C.-H. Luke Ong (eds.) |
Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Steffen van Bakel, Franco Barbanera, Ugo de'Liguoro |
A Filter Model for the λμ-Calculus - (Extended Abstract). |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski |
Partiality, State and Dependent Types. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Ashish Tiwari 0001 |
Rewriting in Practice. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Luca Roversi |
Linear Lambda Calculus and Deep Inference. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Reuben N. S. Rowe, Steffen van Bakel |
Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming - (Extended Abstract). |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Zena M. Ariola, Hugo Herbelin, Alexis Saurin |
Classical Call-by-Need and Duality. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jakob Rehof, Pawel Urzyczyn |
Finite Combinatory Logic with Intersection Types. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Pierre Clairambault, Peter Dybjer |
The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Stephanie Weirich |
Combining Proofs and Programs. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexandre Miquel |
A Survey of Classical Realizability. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Stéphane Gimenez |
Realizability Proof for Normalization of Full Differential Linear Logic. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Antoine Madet, Roberto M. Amadio |
An Elementary Affine λ-Calculus with Multithreading and Side Effects. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Arndt 0001, Krzysztof Kapulkin |
Homotopy-Theoretic Models of Type Theory. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Aloïs Brunel, Olivier Hermant, Clément Houtmann |
Orthogonality and Boolean Algebras for Deduction Modulo. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Sophie Tison |
Tree Automata, (Dis-)Equality Constraints and Term Rewriting - What's New? |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Pierre Bourreau, Sylvain Salvati |
Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed λ-Calculus. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Giulio Manzonetto, Michele Pagani |
Böhm's Theorem for Resource Lambda Calculus through Taylor Expansion. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Abel 0001, Brigitte Pientka |
Higher-Order Dynamic Pattern Unification for Dependent Types and Records. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Marc Lasson |
Controlling Program Extraction in Light Logics. |
TLCA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Atkey |
Syntax for Free: Representing Syntax with Binding Using Parametricity. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Claudia Faggian, Mauro Piccolo |
Partial Orders, Event Structures and Linear Strategies. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Barbara Petit |
A Polymorphic Type System for the Lambda-Calculus with Constructors. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
strong normalisation, pattern matching, polymorphism, lambda-calculus |
| 1 | Andreas Abel 0001, Thierry Coquand, Miguel Pagano |
A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Michele Basaldella, Kazushige Terui |
On the Meaning of Logical Completeness. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Yu Zhang |
The Computational SLR: A Logic for Reasoning about Computational Indistinguishability. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter LeFanu Lumsdaine |
Weak omega-Categories from Intensional Type Theory. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Christine Tasson |
Algebraic Totality, towards Completeness. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Dimitris Mostrous, Nobuko Yoshida |
Session-Based Communication Optimisation for Higher-Order Mobile Processes. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Colin Riba |
On the Values of Reducibility Candidates. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexandre Miquel |
Relating Classical Realizability and Negative Translation for Existential Witness Extraction. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Florian Stenger, Janis Voigtländer |
Parametricity for Haskell with Imprecise Error Semantics. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Michele Pagani |
The Cut-Elimination Theorem for Differential Nets with Promotion. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Ken-etsu Fujita, Aleksy Schubert |
Existential Type Systems with No Types in Terms. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Ugo Dal Lago, Martin Hofmann 0001 |
Bounded Linear Logic, Revisited. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Pawel Urzyczyn |
Inhabitation of Low-Rank Intersection Types. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Pierre-Louis Curien (eds.) |
Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Pierre Boudes |
Thick Subtrees, Games and Experiments. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Harper 0001, Daniel R. Licata, Noam Zeilberger |
A Pronominal Approach to Binding and Computation. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Hugo Herbelin, Stéphane Zimmermann |
An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction" Form. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Lionel Vaux |
Differential Linear Logic and Polarization. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Makoto Hamana |
Initial Algebra Semantics for Cyclic Sharing Structures. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Federico Aschieri, Stefano Berardi |
Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Takeshi Tsukada, Atsushi Igarashi |
A Logical Foundation for Environment Classifiers. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Steven Awodey, Florian Rabe 0001 |
Kripke Semantics for Martin-Löf's Extensional Type Theory. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | William Lovas, Frank Pfenning |
Refinement Types as Proof Irrelevance. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Marcelo P. Fiore, Chung-Kil Hur |
Mathematical Synthesis of Equational Deduction Systems. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Gunnar Wilken, Andreas Weiermann |
Complexity of Gödel's T in lambda-Formulation. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
Typed ?-Calculus, Gödel’s T, Termination, Rewrite System, Strong Normalization |
| 1 | Jeffrey Sarnat, Carsten Schürmann 0001 |
Lexicographic Path Induction. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Lutz Straßburger |
Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic. |
TLCA |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Bove, Venanzio Capretta |
Computation by Prophecy. |
TLCA |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Claudia Faggian, Mauro Piccolo |
Ludics is a Model for the Finitary Linear Pi-Calculus. |
TLCA |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | José Espírito Santo |
Completing Herbelin's Programme. |
TLCA |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Dariusz Kusmierek |
The Inhabitation Problem for Rank Two Intersection Types. |
TLCA |
2007 |
DBLP DOI BibTeX RDF |
type inhabitation problem, lambda calculus, intersection types, alternating Turing machine |
| 1 | Oleg Kiselyov, Chung-chieh Shan |
A Substructural Type System for Delimited Continuations. |
TLCA |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Damiano Mazza |
Edifices and Full Abstraction for the Symmetric Interaction Combinators. |
TLCA |
2007 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license