Typed Lambda Calculi and Applications

Inhaltsverzeichnis

• Termination and Productivity Checking with Continuous Types.
• Derivatives of Containers.
• Max-Plus Quasi-interpretations.
• Inductive Types in the Calculus of Algebraic Constructions.
• On Strong Normalization in the Intersection Type Discipline.
• Relative Definability and Models of Unary PCF.
• Principal Typing in Elementary Affine Logic.
• A Logical Framework with Dependently Typed Records.
• A Sound and Complete CPS-Translation for ??-Calculus.
• Abstraction Barrier-Observing Relational Parametricity.
• Encoding of the Halting Problem into the Monster Type and Applications.
• Well-Going Programs Can Be Typed.
• Parameterizations and Fixed-Point Operators on Control Categories.
• Functional In-Place Update with Layered Datatype Sharing.
• A Fully Abstract Bidomain Model of Unary FPC.
• On a Semantic Definition of Data Independence.
• Nondeterministic Light Logics and NP-Time.
• Polarized Proof Nets with Cycles and Fixpoints Semantics.
• Observational Equivalence and Program Extraction in the Coq Proof Assistant.
• Permutative Conversions in Intuitionistic Multiary Sequent Calculi with Cuts.
• A Universal Embedding for the Higher Order Structure of Computational Effects.