You have Guest access.
Log In
Marc Bezem and Jan Friso Groote
Front matter
1-12
On Mints' reduction for ccc-calculus
13-28
A formalization of the strong normalization proof for System F in LEGO
29-44
Partial intersection type assignment in applicative term rewriting systems
45-59
Extracting constructive content from classical logic via control-like reductions
60-74
Combining first and higher order rewrite systems with type assignment systems
75-90
A term calculus for Intuitionistic Linear Logic
91-106
Program extraction from normalization proofs
107-123
A semantics for λ &-early: a calculus with overloading and early binding Extended abstract
124-138
An abstract notion of application
139-145
The undecidability of typability in the Lambda-Pi-calculus
146-162
Recursive types are not conservative over F≤ Extended abstract
163-178
The conservation theorem revisited
179-194
Modified realizability toposes and strong normalization proofs Extended abstract
195-208
Semantics of lambda-I and of other substructure lambda calculi
209-229
Translating dependent type theory into higher order logic
230-244
Studying the fully abstract model of PCF within its continuous function model
245-257
A new characterization of lambda definability
258-273
Combining recursive and dynamic types
274-288
Lambda calculus characterizations of poly-time
289-305
Pure type systems formalized
306-317
Orthogonal higher-order rewrite systems are confluent
318-327
Monotonic versus antimonotonic exponentiation
328-345
Inductive definitions in the system Coq rules and properties
346-360
Intersection types and bounded polymorphism
361-375
A logic for parametric polymorphism
376-390
Call-by-value and nondeterminism
391-405
Lower and upper bounds for reductions of types in λ and λP (extended abstract)
406-417
λ-Calculi with conditional rules
418-432
Type reconstruction in Fω is undecidable
Back matter
Yohji Akama
Thorsten Altenkirch
Steffen van Bakel
Franco Barbanera and Stefano Berardi
Franco Barbanera and Maribel Fernández
Nick Benton, Gavin Bierman, Valeria de Paiva and Martin Hyland
Ulrich Berger
Giuseppe Castagna, Giorgio Ghelli and Giuseppe Longo
Pietro Di Gianantonio and Furio Honsell
Gilles Dowek
Giorgio Ghelli
Philippe Groote
J. M. E. Hyland and C. -H. L. Ong
Bart Jacobs
Bart Jacobs and Tom Melham
Achim Jung and Allen Stoughton
Achim Jung and Jerzy Tiuryn
Hans Leiß
Daniel Leivant and Jean-Yves Marion
James McKinna and Robert Pollack
Tobias Nipkow
Daniel F. Otth
Christine Paulin-Mohring
Benjamin C. Pierce
Gordon Plotkin and Martín Abadi
Kurt Sieber
Jan Springintveld
Masako Takahashi
Paweł Urzyczyn
Frequently asked questions General info on journals and books Send us your feedback Impressum Contact us
© Springer, Part of Springer Science+Business Media Privacy, Disclaimer, Terms & Conditions, and Copyright Info