3. ITP 2012:
Princeton, NJ, USA
Invited Talks
André Platzer:
A Differential Operator Approach to Equational Differential Invariants - (Invited Paper).
28-48
Invited Tutorial
Formalization of Mathematics I
Cyril Cohen:
Construction of Real Algebraic Numbers in Coq.
67-82
Program Abstraction and Logics
Tobias Nipkow:
Abstract Interpretation of Annotated Commands.
116-132
Data Structures and Synthesis
Security
(Non-)Termination and Automata
Andrea Asperti:
A Compact Proof of Decidability for Regular Expression Equivalence.
283-298
Program Verification
Rough Diamonds I:
Reasoning about Program Execution
Theorem Prover Development
Formalization of Mathematics II
Lars Noschinski:
Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem.
393-404
Rough Diamonds II:
Prover Infrastructure and Modeling Styles
Magnus O. Myreen:
Functional Programs: Conversions between Deep and Shallow Embeddings.
412-417
data released under the ODC-BY 1.0 license
