default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID9th TLCA 2009: Brasilia, Brazil
- Pierre-Louis Curien:
Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings. Lecture Notes in Computer Science 5608, Springer 2009, ISBN 978-3-642-02272-2 - Marcelo P. Fiore, Chung-Kil Hur:
Mathematical Synthesis of Equational Deduction Systems. 1-2 - Robert Harper, Daniel R. Licata
, Noam Zeilberger:
A Pronominal Approach to Binding and Computation. 3-4 - Andreas Abel, Thierry Coquand, Miguel Pagano:
A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance. 5-19 - Federico Aschieri, Stefano Berardi:
Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM1. 20-34 - Robert Atkey:
Syntax for Free: Representing Syntax with Binding Using Parametricity. 35-49 - Michele Basaldella, Kazushige Terui:
On the Meaning of Logical Completeness. 50-64 - Pierre Boudes:
Thick Subtrees, Games and Experiments. 65-79 - Ugo Dal Lago, Martin Hofmann:
Bounded Linear Logic, Revisited. 80-94 - Claudia Faggian, Mauro Piccolo:
Partial Orders, Event Structures and Linear Strategies. 95-111 - Ken-etsu Fujita, Aleksy Schubert:
Existential Type Systems with No Types in Terms. 112-126 - Makoto Hamana:
Initial Algebra Semantics for Cyclic Sharing Structures. 127-141 - Hugo Herbelin, Stéphane Zimmermann:
An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction" Form. 142-156 - William Lovas, Frank Pfenning:
Refinement Types as Proof Irrelevance. 157-171 - Peter LeFanu Lumsdaine:
Weak omega-Categories from Intensional Type Theory. 172-187 - Alexandre Miquel:
Relating Classical Realizability and Negative Translation for Existential Witness Extraction. 188-202 - Dimitris Mostrous, Nobuko Yoshida:
Session-Based Communication Optimisation for Higher-Order Mobile Processes. 203-218 - Michele Pagani:
The Cut-Elimination Theorem for Differential Nets with Promotion. 219-233 - Barbara Petit:
A Polymorphic Type System for the Lambda-Calculus with Constructors. 234-248 - Steven Awodey, Florian Rabe:
Kripke Semantics for Martin-Löf's Extensional Type Theory. 249-263 - Colin Riba:
On the Values of Reducibility Candidates. 264-278 - Jeffrey Sarnat, Carsten Schürmann:
Lexicographic Path Induction. 279-293 - Florian Stenger, Janis Voigtländer:
Parametricity for Haskell with Imprecise Error Semantics. 294-308 - Lutz Straßburger:
Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic. 309-324 - Christine Tasson:
Algebraic Totality, towards Completeness. 325-340 - Takeshi Tsukada, Atsushi Igarashi:
A Logical Foundation for Environment Classifiers. 341-355 - Pawel Urzyczyn:
Inhabitation of Low-Rank Intersection Types. 356-370 - Lionel Vaux:
Differential Linear Logic and Polarization. 371-385 - Gunnar Wilken, Andreas Weiermann:
Complexity of Gödel's T in lambda-Formulation. 386-400 - Yu Zhang:
The Computational SLR: A Logic for Reasoning about Computational Indistinguishability. 401-415
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-11-28 23:52 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
