ITP 2014 LNCS PROCEEDINGS: AUTHOR INDEX

Papers Papers with Abstracts Preface Author Index Keyword Index

Shortcuts: A B C D E G H K L M N O P R S T V W X

A
Anand, Abhishek	Towards a Formally Verified Proof Assistant (PDF, talk)
Aravantinos, Vincent	Implicational Rewriting Tactics in HOL (PDF, talk) Formal Verification of Optical Quantum Flip Gate (PDF, talk)
Arthan, Rob	HOL with Definitions: Semantics, Soundness, and a Verified Implementation (PDF, talk) HOL Constant Definitions Done Right (PDF, talk)
Avigad, Jeremy	A heuristic prover for real inequalities (PDF, talk)
B
Bartzia, Evmorfia-Iro	A Formal Library for Elliptic Curves in the Coq Proof Assistant (PDF, talk)
Blanchette, Jasmin Christian	Truly Modular (Co)datatypes for Isabelle/HOL (PDF, talk) Cardinals in Isabelle/HOL (PDF, talk)
Blazy, Sandrine	Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code (PDF, talk)
Bourke, Timothy	Showing invariance compositionally for a process algebra for network protocols (PDF, talk)
Braibant, Thomas	Compositional Computational Reflection (PDF, talk)
C
Chapman, Rod	Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK (PDF, talk)
Chlipala, Adam	Experience Implementing a Performant Category-Theory Library in Coq (PDF, talk) Compositional Computational Reflection (PDF, talk)
Chyzak, Frédéric	A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) (PDF, talk)
Cock, David	From Operational Models to Information Theory - Side Channels in pGCL with Isabelle (PDF, talk)
Cohen, Cyril	A Coq Formalization of Finitely Presented Modules (PDF, talk)
D
Davis, Jared	The reflective Milawa theorem prover is sound (down to the machine code that runs it) (PDF, talk)
Davis, Jared	Microcode Verification - Another Piece of the Microprocessor Verification Puzzle (PDF, talk)
Dockins, Robert	Formalized, effective domain theory in Coq (PDF, talk)
Doczkal, Christian	Completeness and Decidability Results for CTL in Coq (PDF, talk)
Dufourd, Jean-François	Hypermap Specification and Certified Linked Implementation using Orbits (PDF, talk)
E
Emoto, Kento	A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction (PDF, talk)
G
Gross, Jason	Experience Implementing a Performant Category-Theory Library in Coq (PDF, talk)
H
Hao, Kecheng	Mechanical Certification of Loop Pipelining Transformations: A Preview (PDF, talk)
Hirokawa, Nao	A New and Formalized Proof of Abstract Completion (PDF, talk)
Höfner, Peter	Showing invariance compositionally for a process algebra for network protocols (PDF, talk)
Hölzl, Johannes	Truly Modular (Co)datatypes for Isabelle/HOL (PDF, talk) Recursive Functions on Lazy Lists via Domains and Topologies (PDF, talk)
K
Kaufmann, Matt	Rough Diamond: An Extension of Equivalence-based Rewriting (PDF, talk)
Krebbers, Robbert	Formal C semantics: CompCert and the C standard (PDF, talk)
Kumar, Ramana	HOL with Definitions: Semantics, Soundness, and a Verified Implementation (PDF, talk)
L
Lammich, Peter	Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm (PDF, talk)
Laporte, Vincent	Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code (PDF, talk)
Leroy, Xavier	Formal C semantics: CompCert and the C standard (PDF, talk)
Lewis, Robert Y.	A heuristic prover for real inequalities (PDF, talk)
Lochbihler, Andreas	Truly Modular (Co)datatypes for Isabelle/HOL (PDF, talk) Recursive Functions on Lazy Lists via Domains and Topologies (PDF, talk)
Loulergue, Frédéric	A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction (PDF, talk)
Lüth, Christoph	Collaborative Interactive Theorem Proving with Clide (PDF, talk)
M
Mahboubi, Assia	A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) (PDF, talk)
Mahmoud, Mohamed Yousri	Formal Verification of Optical Quantum Flip Gate (PDF, talk) On the Formalization of Z-Transform in HOL (PDF, talk)
Malecha, Gregory	Compositional Computational Reflection (PDF, talk)
Matichuk, Daniel	An Isabelle Proof Method Language (PDF, talk)
Middeldorp, Aart	A New and Formalized Proof of Abstract Completion (PDF, talk)
Moore, J Strother	Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete (PDF, talk) Rough Diamond: An Extension of Equivalence-based Rewriting (PDF, talk)
Murray, Toby	An Isabelle Proof Method Language (PDF, talk)
Myreen, Magnus O.	HOL with Definitions: Semantics, Soundness, and a Verified Implementation (PDF, talk) The reflective Milawa theorem prover is sound (down to the machine code that runs it) (PDF, talk)
Mörtberg, Anders	A Coq Formalization of Finitely Presented Modules (PDF, talk)
N
Naves, Guyslain	Balancing lists: a proof pearl (PDF, talk)
Nipkow, Tobias	Unified Decision Procedures for Regular Expression Equivalence (PDF, talk)
O
Owens, Scott	HOL with Definitions: Semantics, Soundness, and a Verified Implementation (PDF, talk)
P
Panny, Lorenz	Truly Modular (Co)datatypes for Isabelle/HOL (PDF, talk)
Pichardie, David	Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code (PDF, talk)
Popescu, Andrei	Truly Modular (Co)datatypes for Isabelle/HOL (PDF, talk) Cardinals in Isabelle/HOL (PDF, talk)
Puri, Disha	Mechanical Certification of Loop Pipelining Transformations: A Preview (PDF, talk)
R
Rahli, Vincent	Towards a Formally Verified Proof Assistant (PDF, talk)
Ray, Sandip	Mechanical Certification of Loop Pipelining Transformations: A Preview (PDF, talk)
Ring, Martin	Collaborative Interactive Theorem Proving with Clide (PDF, talk)
Roux, Cody	A heuristic prover for real inequalities (PDF, talk)
S
Schanda, Florian	Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK (PDF, talk)
Sewell, Peter	Retrofitting Rigour (PDF, talk)
Sibut-Pinote, Thomas	A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) (PDF, talk)
Siddique, Umair	On the Formalization of Z-Transform in HOL (PDF, talk)
Slobodova, Anna	Microcode Verification - Another Piece of the Microprocessor Verification Puzzle (PDF, talk)
Smolka, Gert	Completeness and Decidability Results for CTL in Coq (PDF, talk)
Sozeau, Matthieu	Universe Polymorphism in Coq (PDF, talk)
Spivak, David	Experience Implementing a Performant Category-Theory Library in Coq (PDF, talk)
Spiwack, Arnaud	Balancing lists: a proof pearl (PDF, talk)
Sternagel, Christian	A New and Formalized Proof of Abstract Completion (PDF, talk)
Strub, Pierre-Yves	A Formal Library for Elliptic Curves in the Coq Proof Assistant (PDF, talk)
Swords, Sol	Microcode Verification - Another Piece of the Microprocessor Verification Puzzle (PDF, talk)
T
Tabareau, Nicolas	Universe Polymorphism in Coq (PDF, talk)
Tahar, Sofiene	Implicational Rewriting Tactics in HOL (PDF, talk) Formal Verification of Optical Quantum Flip Gate (PDF, talk) On the Formalization of Z-Transform in HOL (PDF, talk)
Tassi, Enrico	A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) (PDF, talk)
Tesson, Julien	A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction (PDF, talk)
Traytel, Dmitriy	Truly Modular (Co)datatypes for Isabelle/HOL (PDF, talk) Cardinals in Isabelle/HOL (PDF, talk) Unified Decision Procedures for Regular Expression Equivalence (PDF, talk)
V
Van Glabbeek, Rob	Showing invariance compositionally for a process algebra for network protocols (PDF, talk)
W
Wenzel, Makarius	An Isabelle Proof Method Language (PDF, talk) Asynchronous User Interaction and Tool Integration in Isabelle/PIDE (PDF, talk)
Wiedijk, Freek	Formal C semantics: CompCert and the C standard (PDF, talk)
X
Xie, Fei	Mechanical Certification of Loop Pipelining Transformations: A Preview (PDF, talk)