VSL 2014: VIENNA SUMMER OF LOGIC 2014

This page contains an index consisting of author-provided keywords.

A
abstract interpretation	Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code
ACL2	Rough Diamond: An Extension of Equivalence-based Rewriting The reflective Milawa theorem prover is sound (down to the machine code that runs it) Mechanical Certification of Loop Pipelining Transformations: A Preview Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete
Agda	Towards a Formally Verified Proof Assistant
Algebraic specification	Hypermap Specification and Certified Linked Implementation using Orbits
Apéry constant	A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
automatic program calculation	A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
automation	Implicational Rewriting Tactics in HOL Compositional Computational Reflection
B
Beam Splitter	Formal Verification of Optical Quantum Flip Gate
Behavioral Synthesis	Mechanical Certification of Loop Pipelining Transformations: A Preview
Brzozowski derivatives	Unified Decision Procedures for Regular Expression Equivalence
bulk synchronous parallelism	A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
C
cardinal number	Cardinals in Isabelle/HOL
category theory	Experience Implementing a Performant Category-Theory Library in Coq
codatatypes	Recursive Functions on Codatatypes via Domains and Topologies
Coherent Light	Formal Verification of Optical Quantum Flip Gate
Combinatorial hypermap library	Hypermap Specification and Certified Linked Implementation using Orbits
Compiler certification	Formal C semantics: CompCert and the C standard
complete partial orders	Recursive Functions on Codatatypes via Domains and Topologies
completeness	Completeness and Decidability Results for CTL in Coq
completion	A New and Formalized Proof of Abstract Completion
computational reflection	Compositional Computational Reflection
computer algebra	A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
computer-supported collaborative work	Collaborative Interactive Theorem Proving with Clide
confluence	A New and Formalized Proof of Abstract Completion
congruence	Rough Diamond: An Extension of Equivalence-based Rewriting
conservative extension	HOL Constant Definitions Done Right
Consistency	Towards a Formally Verified Proof Assistant
Constant Definition	HOL Constant Definitions Done Right
constructive algebra	A Coq Formalization of Finitely Presented Modules
constructive mathematics	Formalized, effective domain theory in Coq
Conversions	Implicational Rewriting Tactics in HOL
Coq	Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code Completeness and Decidability Results for CTL in Coq A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction Towards a Formally Verified Proof Assistant Formal C semantics: CompCert and the C standard Formalized, effective domain theory in Coq A Coq Formalization of Finitely Presented Modules Experience Implementing a Performant Category-Theory Library in Coq Balancing lists: a proof pearl A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) Compositional Computational Reflection
Coq proof assistant	Hypermap Specification and Certified Linked Implementation using Orbits
Coq/SSReflect Proof Assistant	A Formal Library for Elliptic Curves in the Coq Proof Assistant
creative telescoping	A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
CTL	Completeness and Decidability Results for CTL in Coq
D
decidability	Completeness and Decidability Results for CTL in Coq
decision procedure	Unified Decision Procedures for Regular Expression Equivalence
definitional package	Truly Modular (Co)datatypes for Isabelle/HOL
Difference Equations	On the Formalization of Z-Transform in HOL
domain theory	Formalized, effective domain theory in Coq
duality	Experience Implementing a Performant Category-Theory Library in Coq
E
Elliptic Curves	A Formal Library for Elliptic Curves in the Coq Proof Assistant
Emptiness Check for Generalized Buchi Automata	Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm
equivalence relation	Rough Diamond: An Extension of Equivalence-based Rewriting
ESL Design	Mechanical Certification of Loop Pipelining Transformations: A Preview
F
Formal semantics	Formal C semantics: CompCert and the C standard
Formalization of mathematics	A Coq Formalization of Finitely Presented Modules
Full trees	Balancing lists: a proof pearl
functional programming	A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
H
Hierarchized linked implementation	Hypermap Specification and Certified Linked Implementation using Orbits
High Level Synthesis	Mechanical Certification of Loop Pipelining Transformations: A Preview
higher-order logic	Cardinals in Isabelle/HOL On the Formalization of Z-Transform in HOL Truly Modular (Co)datatypes for Isabelle/HOL
Hilbert axiomatizations	Completeness and Decidability Results for CTL in Coq
HOL	HOL with Definitions: Semantics, Soundness, and a Verified Implementation HOL Constant Definitions Done Right
HOL Light	Implicational Rewriting Tactics in HOL On the Formalization of Z-Transform in HOL Formal Verification of Optical Quantum Flip Gate
HOL4	Implicational Rewriting Tactics in HOL
Homological algebra	A Coq Formalization of Finitely Presented Modules
homotopy type theory	Experience Implementing a Performant Category-Theory Library in Coq
I
Implicit Definition	HOL Constant Definitions Done Right
improvements in theorem prover technology	Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
interactive theorem proving	A heuristic prover for real inequalities
invariance proofs	Showing invariance compositionally for a process algebra for network protocols
Invariants	From Operational Models to Information Theory - Side-Channels in pGCL with Isabelle
irrationality proof	A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
Isabelle	From Operational Models to Information Theory - Side-Channels in pGCL with Isabelle An Isabelle Proof Method Language Unified Decision Procedures for Regular Expression Equivalence
Isabelle/HOL	Cardinals in Isabelle/HOL Recursive Functions on Codatatypes via Domains and Topologies A New and Formalized Proof of Abstract Completion Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm Showing invariance compositionally for a process algebra for network protocols Truly Modular (Co)datatypes for Isabelle/HOL
Isabelle/PIDE and Isabelle/jEdit	Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
J
Java Virtual Machine (JVM)	Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete
L
lazy lists	Recursive Functions on Codatatypes via Domains and Topologies
list homomorphisms	A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
low-level programming languages	Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code
M
marked regular expressions	Unified Decision Procedures for Regular Expression Equivalence
mathematical components	A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
Mechanization of Mathematics	A Formal Library for Elliptic Curves in the Coq Proof Assistant
N
network protocols	Showing invariance compositionally for a process algebra for network protocols
Non-uniform inductive types	Balancing lists: a proof pearl
Numerical representations	Balancing lists: a proof pearl
Nuprl	Towards a Formally Verified Proof Assistant
O
OCaml	Balancing lists: a proof pearl
Orbits for functions in finite domains	Hypermap Specification and Certified Linked Implementation using Orbits
ordinal number	Cardinals in Isabelle/HOL
P
partial derivatives	Unified Decision Procedures for Regular Expression Equivalence
Partial Equivalence Relations	Towards a Formally Verified Proof Assistant
Path Based SCC Algorithms	Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm
peak decreasingness	A New and Formalized Proof of Abstract Completion
performance	Experience Implementing a Performant Category-Theory Library in Coq
pGCL	From Operational Models to Information Theory - Side-Channels in pGCL with Isabelle
Phase Conjugating Mirror	Formal Verification of Optical Quantum Flip Gate
Polya	A heuristic prover for real inequalities
prime critical pairs	A New and Formalized Proof of Abstract Completion
process algebra	Showing invariance compositionally for a process algebra for network protocols
proof automation	An Isabelle Proof Method Language
Proof of topological properties	Hypermap Specification and Certified Linked Implementation using Orbits
Proof of total correctness	Hypermap Specification and Certified Linked Implementation using Orbits
Proof pearl	Balancing lists: a proof pearl
proof procedure language	An Isabelle Proof Method Language
Q
Quantum Flip Gate	Formal Verification of Optical Quantum Flip Gate
Quantum Optics	Formal Verification of Optical Quantum Flip Gate
R
reactive systems	Showing invariance compositionally for a process algebra for network protocols
real inequalities	A heuristic prover for real inequalities
recursion	Recursive Functions on Codatatypes via Domains and Topologies
refinement	Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm
reflection	The reflective Milawa theorem prover is sound (down to the machine code that runs it)
regular expression equivalence	Unified Decision Procedures for Regular Expression Equivalence
Rewriting	Rough Diamond: An Extension of Equivalence-based Rewriting Implicational Rewriting Tactics in HOL
RTL	Mechanical Certification of Loop Pipelining Transformations: A Preview
S
Security	From Operational Models to Information Theory - Side-Channels in pGCL with Isabelle
semantics	HOL with Definitions: Semantics, Soundness, and a Verified Implementation Towards a Formally Verified Proof Assistant The reflective Milawa theorem prover is sound (down to the machine code that runs it)
semi-ring computation	A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
soundness	HOL with Definitions: Semantics, Soundness, and a Verified Implementation The reflective Milawa theorem prover is sound (down to the machine code that runs it)
SSReflect	Completeness and Decidability Results for CTL in Coq A Coq Formalization of Finitely Presented Modules A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
Strongly Connected Components	Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm
subtyping	Universe Polymorphism in Coq
T
tableaux	Completeness and Decidability Results for CTL in Coq
tactics	Implicational Rewriting Tactics in HOL
temporal logics	Completeness and Decidability Results for CTL in Coq
term rewriting	A New and Formalized Proof of Abstract Completion
theorem prover technology	Collaborative Interactive Theorem Proving with Clide
theorem proving	Formal Verification of Optical Quantum Flip Gate Mechanical Certification of Loop Pipelining Transformations: A Preview
theorem-prover implementation	The reflective Milawa theorem prover is sound (down to the machine code that runs it)
topology	Recursive Functions on Codatatypes via Domains and Topologies
Transformation Analysis	On the Formalization of Z-Transform in HOL
Turing machine	Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete
type theory	Universe Polymorphism in Coq
U
Unification	Universe Polymorphism in Coq
universes	Universe Polymorphism in Coq
user interfaces for interactive theorem provers	Asynchronous User Interaction and Tool Integration in Isabelle/PIDE Collaborative Interactive Theorem Proving with Clide
V
verifying compiler	Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete
W
wellorder	Cardinals in Isabelle/HOL
Z
Z-Transform	On the Formalization of Z-Transform in HOL

Disclaimer | Powered by EasyChair Smart Program