Andreas Abel (auth.), Martin Hofmann (eds.)3540403329, 9783540403326
The 21 revised full papers presented were carefully reviewed and selected from 40 submissions. The volume reports research results on all current aspects of typed lambda calculi, ranging from theoretical and methodological issues to the application of proof assistants.
Table of contents :
Termination and Productivity Checking with Continuous Types….Pages 1-15
Derivatives of Containers….Pages 16-30
Max-Plus Quasi-interpretations….Pages 31-45
Inductive Types in the Calculus of Algebraic Constructions….Pages 46-59
On Strong Normalization in the Intersection Type Discipline….Pages 60-74
Relative Definability and Models of Unary PCF….Pages 75-89
Principal Typing in Elementary Affine Logic….Pages 90-104
A Logical Framework with Dependently Typed Records….Pages 105-119
A Sound and Complete CPS-Translation for λμ-Calculus….Pages 120-134
Abstraction Barrier-Observing Relational Parametricity….Pages 135-152
Encoding of the Halting Problem into the Monster Type and Applications….Pages 153-166
Well-Going Programs Can Be Typed….Pages 167-179
Parameterizations and Fixed-Point Operators on Control Categories….Pages 180-194
Functional In-Place Update with Layered Datatype Sharing….Pages 195-210
A Fully Abstract Bidomain Model of Unary FPC….Pages 211-225
On a Semantic Definition of Data Independence….Pages 226-240
Nondeterministic Light Logics and NP-Time….Pages 241-255
Polarized Proof Nets with Cycles and Fixpoints Semantics….Pages 256-270
Observational Equivalence and Program Extraction in the Coq Proof Assistant….Pages 271-285
Permutative Conversions in Intuitionistic Multiary Sequent Calculi with Cuts….Pages 286-300
A Universal Embedding for the Higher Order Structure of Computational Effects….Pages 301-315
Reviews
There are no reviews yet.