You have Guest access.
Log In
Otmane Ait Mohamed, César Muñoz and Sofiène Tahar
Front matter
1-5
Twenty Years of Theorem Proving for HOLs Past, Present and Future
6-11
Will This Be Formal?
12-16
A Short Presentation of Coq
17-21
An ACL2 Tutorial
22-27
A Brief Overview of PVS
28-32
A Brief Overview of HOL4
33-38
The Isabelle Framework
39-54
A Compiled Implementation of Normalization by Evaluation
55-70
LCF-Style Propositional Simplification with BDDs and SAT Solvers
71-85
Nominal Inversion Principles
86-101
Canonical Big Operators
102-117
A Type of Partial Recursive Functions
118-133
Formal Reasoning About Causality Analysis
134-149
Imperative Functional Programming with Isabelle/HOL
150-166
HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
167-182
Secure Microkernels, State Monads and Scalable Refinement
183-198
Certifying a Termination Criterion Based on Graphs, without Graphs
199-214
Lightweight Separation
215-229
Real Number Calculations and Theorem Proving Validation and Use of an Exact Arithmetic
230-245
A Formalized Theory for Verifying Stability and Convergence of Automata in PVS
246-261
Certified Exact Transcendental Real Number Computation in Coq
262-277
Formalizing Soundness of Contextual Effects
278-293
First-Class Type Classes
294-309
Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL
310-319
Proof Pearl: Revisiting the Mini-rubik in Coq
Back matter
This page requires script.
Frequently asked questions General info on journals and books Send us your feedback Impressum Contact us
© Springer, Part of Springer Science+Business Media Privacy, Disclaimer, Terms & Conditions, and Copyright Info