default search action
7th TLCA 2005: Nara, Japan
- Pawel Urzyczyn:
Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings. Lecture Notes in Computer Science 3461, Springer 2005, ISBN 3-540-25593-1 - Thierry Coquand:
Completeness Theorems and lambda-Calculus. 1-9 - Amy P. Felty:
A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code: Abstract. 10-10 - Susumu Hayashi:
Can Proofs Be Animated By Games? 11-22
Contributed Papers
- Andreas Abel, Thierry Coquand:
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. 23-38 - Klaus Aehlig, Jolie G. de Miranda, C.-H. Luke Ong
:
The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable. 39-54 - Patrick Baillot, Kazushige Terui:
A Feasible Algorithm for Typing in Elementary Affine Logic. 55-70 - Gilles Barthe, Benjamin Grégoire, Fernando Pastawski
Practical Inference for Type-Based Termination in a Polymorphic Setting. 71-85 - Nick Benton, Benjamin Leperchey:
Relational Reasoning in a Nominal Semantics for Storage. 86-101 - Yves Bertot:
Filters on CoInductive Streams, an Application to Eratosthenes' Sieve. 102-115 - Ana Bove
Recursive Functions with Higher Order Domains. 116-130 - Paolo Coppola, Ugo Dal Lago, Simona Ronchi Della Rocca:
Elementary Affine Logic and the Call-by-Value Lambda Calculus. 131-145 - Ferruccio Damiani:
Rank-2 Intersection and Polymorphic Recursion. 146-161 - René David, Karim Nour:
Arithmetical Proofs of Strong Normalization Results for the Symmetric lambda-µ-Calculus. 162-178 - Roberto Di Cosmo, François Pottier, Didier Rémy:
Subtyping Recursive Types Modulo Associative Commutative Products. 179-193 - Ken-etsu Fujita:
Galois Embedding from Polymorphic Types into Existential Types. 194-208 - Hugo Herbelin:
On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic. 209-220 - Olivier Hermant:
Semantic Cut Elimination in the Intuitionistic Sequent Calculus. 221-233 - James Laird
The Elimination of Nesting in SPCF. 234-245 - François Lamarche, Lutz Straßburger:
Naming Proofs in Classical Propositional Logic. 246-261 - Sam Lindley, Ian Stark
Reducibility and TT-Lifting for Computation Types. 262-277 - Stan Matwin, Amy P. Felty, István T. Hernádvölgyi, Venanzio Capretta
Privacy in Data Mining Using Formal Methods. 278-292 - Greg Morrisett, Amal J. Ahmed, Matthew Fluet:
L3: A Linear Language with Locations. 293-307 - John Power
Binding Signatures for Generic Contexts. 308-323 - Virgile Prevosto
Proof Contexts with Late Binding. 324-338 - Carsten Schürmann, Adam Poswolsky, Jeffrey Sarnat:
The [triangle]-Calculus. Functional Programming with Higher-Order Encodings. 339-353 - Peter Selinger
A Lambda Calculus for Quantum Computation with Classical Control. 354-368 - Paula Severi, Fer-Jan de Vries:
Continuity and Discontinuity in Lambda Calculus. 369-385 - François-Régis Sinot:
Call-by-Name and Call-by-Value as Token-Passing Interaction Nets. 386-400 - Christian Urban, James Cheney
Avoiding Equivariance in Alpha-Prolog. 401-416 - Damiano Zanardini
Higher-Order Abstract Non-interference. 417-432
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 2024-11-22 19:31 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: