Abstract is missing.
- Completeness Theorems and lambda-CalculusThierry Coquand. 1-9 [doi]
- A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code: AbstractAmy P. Felty. 10-10 [doi]
- Can Proofs Be Animated By Games?Susumu Hayashi. 11-22 [doi]
- Untyped Algorithmic Equality for Martin-Löf s Logical Framework with Surjective PairsAndreas Abel, Thierry Coquand. 23-38 [doi]
- The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is DecidableKlaus Aehlig, Jolie G. de Miranda, C.-H. Luke Ong. 39-54 [doi]
- A Feasible Algorithm for Typing in Elementary Affine LogicPatrick Baillot, Kazushige Terui. 55-70 [doi]
- Practical Inference for Type-Based Termination in a Polymorphic SettingGilles Barthe, Benjamin Grégoire, Fernando Pastawski. 71-85 [doi]
- Relational Reasoning in a Nominal Semantics for StorageNick Benton, Benjamin Leperchey. 86-101 [doi]
- Filters on CoInductive Streams, an Application to Eratosthenes SieveYves Bertot. 102-115 [doi]
- Recursive Functions with Higher Order DomainsAna Bove, Venanzio Capretta. 116-130 [doi]
- Elementary Affine Logic and the Call-by-Value Lambda CalculusPaolo Coppola, Ugo Dal Lago, Simona Ronchi Della Rocca. 131-145 [doi]
- Rank-2 Intersection and Polymorphic RecursionFerruccio Damiani. 146-161 [doi]
- Arithmetical Proofs of Strong Normalization Results for the Symmetric lambda-µ-CalculusRené David, Karim Nour. 162-178 [doi]
- Subtyping Recursive Types Modulo Associative Commutative ProductsRoberto Di Cosmo, François Pottier, Didier Rémy. 179-193 [doi]
- Galois Embedding from Polymorphic Types into Existential TypesKen-etsu Fujita. 194-208 [doi]
- On the Degeneracy of Sigma-Types in Presence of Computational Classical LogicHugo Herbelin. 209-220 [doi]
- Semantic Cut Elimination in the Intuitionistic Sequent CalculusOlivier Hermant. 221-233 [doi]
- The Elimination of Nesting in SPCFJames Laird. 234-245 [doi]
- Naming Proofs in Classical Propositional LogicFrançois Lamarche, Lutz Straßburger. 246-261 [doi]
- Reducibility and TT-Lifting for Computation TypesSam Lindley, Ian Stark. 262-277 [doi]
- Privacy in Data Mining Using Formal MethodsStan Matwin, Amy P. Felty, István T. Hernádvölgyi, Venanzio Capretta. 278-292 [doi]
- L:::3:::: A Linear Language with LocationsGreg Morrisett, Amal J. Ahmed, Matthew Fluet. 293-307 [doi]
- Binding Signatures for Generic ContextsJohn Power, Miki Tanaka. 308-323 [doi]
- Proof Contexts with Late BindingVirgile Prevosto, Sylvain Boulmé. 324-338 [doi]
- The [triangle]-Calculus. Functional Programming with Higher-Order EncodingsCarsten Schürmann, Adam Poswolsky, Jeffrey Sarnat. 339-353 [doi]
- A Lambda Calculus for Quantum Computation with Classical ControlPeter Selinger, Benoît Valiron. 354-368 [doi]
- Continuity and Discontinuity in Lambda CalculusPaula Severi, Fer-Jan de Vries. 369-385 [doi]
- Call-by-Name and Call-by-Value as Token-Passing Interaction NetsFrançois-Régis Sinot. 386-400 [doi]
- Avoiding Equivariance in Alpha-PrologChristian Urban, James Cheney. 401-416 [doi]
- Higher-Order Abstract Non-interferenceDamiano Zanardini. 417-432 [doi]