Abstract is missing.
- Type Inference by Coinductive Logic ProgrammingDavide Ancona, Giovanni Lagorio, Elena Zucca. 1-18 [doi]
- About the Formalization of Some Results by Chebyshev in Number TheoryAndrea Asperti, Wilmer Ricciotti. 19-31 [doi]
- A New Elimination Rule for the Calculus of Inductive ConstructionsBruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini. 32-48 [doi]
- A Framework for the Analysis of Access Control Models for Interactive Mobile DevicesJuan Manuel Crespo, Gustavo Betarte, Carlos Luna. 49-63 [doi]
- Proving Infinitary NormalizationJörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, Roel C. de Vrijer. 64-82 [doi]
- First-Class Object SetsErik Ernst. 83-99 [doi]
- Monadic Translation of Intuitionistic Sequent CalculusJosé Espírito Santo, Ralph Matthes, Luis Pinto. 100-116 [doi]
- Towards a Type Discipline for Answer Set ProgrammingCamillo Fiorentini, Alberto Momigliano, Mario Ornaghi. 117-135 [doi]
- Type Inference for a Polynomial Lambda CalculusMarco Gaboardi, Simona Ronchi Della Rocca. 136-152 [doi]
- Local Theory Specifications in Isabelle/IsarFlorian Haftmann, Makarius Wenzel. 153-168 [doi]
- Axiom Directed FocusingClément Houtmann. 169-185 [doi]
- A Type System for Usage of Software ComponentsDag Hovland. 186-202 [doi]
- Merging Procedural and Declarative ProofCezary Kaliszyk, Freek Wiedijk. 203-219 [doi]
- Using Structural Recursion for CorecursionYves Bertot, Ekaterina Komendantskaya. 220-236 [doi]
- Manifest Fields and Module Mechanisms in Intensional Type TheoryZhaohui Luo. 237-255 [doi]
- A Machine-Checked Proof of the Average-Case Complexity of Quicksort in CoqEelis van der Weegen, James McKinna. 256-271 [doi]
- Coalgebraic Reasoning in Coq: Bisimulation and the lambda-Coiteration SchemeMilad Niqui. 272-288 [doi]
- A Process-Model for Linear ProgramsLuca Paolini, Mauro Piccolo. 289-305 [doi]
- Some Complexity and Expressiveness Results on Multimodal and Stratified Proof NetsLuca Roversi, Luca Vercelli. 306-322 [doi]