VSL 2014: VIENNA SUMMER OF LOGIC 2014

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

Disclaimer | Powered by EasyChair Smart Program