Abstract is missing.
- Formalized Metatheory with Terms Represented by an Indexed Family of TypesRobin Adams. 1-16 [doi]
- A Content Based Mathematical Search Engine: WhelpAndrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli. 17-32 [doi]
- A Machine-Checked Formalization of the Random Oracle ModelGilles Barthe, Sabrina Tarento. 33-49 [doi]
- Extracting a Normalization Algorithm in Isabelle/HOLStefan Berghofer. 50-65 [doi]
- A Structured Approach to Proving Compiler Optimizations Based on Dataflow AnalysisYves Bertot, Benjamin Grégoire, Xavier Leroy. 66-81 [doi]
- Formalising Bitonic Sort in Type TheoryAna Bove, Thierry Coquand. 82-97 [doi]
- A Semi-reflexive Tactic for (Sub-)Equational ReasoningClaudio Sacerdoti Coen. 98-114 [doi]
- A Uniform and Certified Approach for Two Static AnalysesSolange Coupet-Grimal, William Delobel. 115-137 [doi]
- Solving Two Problems in General Topology Via TypesAdam Grabowski. 138-153 [doi]
- A Tool for Automated Theorem Proving in AgdaFredrik Lindblad, Marcin Benke. 154-169 [doi]
- Surreal Numbers in CoqLionel Elie Mamane. 170-185 [doi]
- A Few Constructions on ConstructorsConor McBride, Healfdene Goguen, James McKinna. 186-200 [doi]
- Tactic-Based Optimized Compilation of Functional ProgramsThomas Meyer, Burkhart Wolff. 201-214 [doi]
- Interfaces as Games, Programs as StrategiesMarkus Michelbrink. 215-231 [doi]
- lamda-Z: Zermelo s Set Theory as a PTS with 4 SortsAlexandre Miquel. 232-251 [doi]
- Exploring the Regular Tree TypesPeter Morris, Thorsten Altenkirch, Conor McBride. 252-267 [doi]
- On Constructive ExistenceMichel Parigot. 268-273 [doi]