Parameterizations and Fixed-Point Operators on Control Categories Y. Kakutani and M. Hasegawa
Inductive types in the Calculus of Algebraic Constructions F. Blanqui
A universal embedding for the higher order structure of computational effects J. Power
Principal Typing in elementary Affine Logic P. Coppola and S. Ronchi della Rocca
Functional In-place Update with Layered Datatype Sharing M. Konecny
Nondederministic Light Logics and NP-Time F. Maurel
On strong normalisation in the intersection type discipline G. Boudol
Observational equivalence and program extraction in the Coq proof assistant N. Oury
Well-Going Programs Can Be Typed S. Kahrs
Relative definability and models of Unary PCF A. Bucciarelli and B. Leperchey and V. Padovani
Derivatives of containers M. Abbott and T. Altenkirch and N. Ghani and C. McBride
A Logical Framework with Dependently Typed Records T. Coquand and R. Pollack and M. Takeyama
A Fully Abstract Bidomain Model of Unary FPC J. Laird
Encoding of the Monster Type into the Halting Problem & Applications T. Joly
Permutative Conversions in Intuitionistic Multiary Sequent Calculi with Cuts L. Pinto and J. Espirito Santo
Proof-Nets with cycles and fixpoint semantics R. Montelatici
On a Semantic Definition of Data Independence R. Lazic and D. Nowak
Max-plus quasi-interpretations R. Amadio
Termination and Productivity Checking with Continuous Types A. Abel
Abstraction Barrier-Observing Relational Parametricity J. Hannay
A sound and complete CPS-translation for lambda-mu-calculus K. Fujita