You have Guest access.
Log In
Yves Bertot, Gilles Dowek, Laurent Théry, André Hirschowitz and Christine Paulin
Front matter
839
Recent Advancements in Hardware Verification — How to Make Theorem Proving Fit for an Industrial Usage
840
Disjoint Sums over Type Classes in HOL
Inductive Datatypes in HOL — Lessons Learned in Formal-Logic Engineering
Isomorphisms — A Link Between the Shallow and the Deep
Polytypic Proof Construction
Recursive Function Definition over Coinductive Types
83
Hardware Verification Using Co-induction in COQ
Connecting Proof Checkers and Computer Algebra Using OpenMath
A Machine-Checked Theory of Floating Point Arithmetic
Universal Algebra in Type Theory
Locales A Sectioning Concept for Isabelle
Isar — A Generic Interpretative Approach to Readable Formal Proof Documents
On the Implementation of an Extensible Declarative Proof Language
Three Tactic Theorem Proving
Mechanized Operational Semantics via (Co)Induction
Representing WP Semantics in Isabelle/ZF
A HOL Conversion for Translating Linear Time Temporal Logic to ω-Automata
From I/O Automata to Timed I/O Automata A Solution to the ‘Generalized Railroad Crossing’ in Isabelle/HOLCF
Formal Methods and Security Evaluation
Importing MDG Verification Results into HOL
Integrating Gandalf and HOL
Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving
Symbolic Functional Evaluation
Back matter
Thomas Kropf
Norbert Völker
Stefan Berghofer and Markus Wenzel
Thomas Santen
Holger Pfeifer and Harald Rueβ
John Matthews
Solange Coupet-Grimal and Line Jakubiec
Olga Caprotti and Arjeh M. Cohen
John Harrison
Venanzio Capretta
Florian Kammüller, Markus Wenzel and Lawrence C. Paulson
Markus Wenzel
Vincent Zammit
Don Syme
Simon J. Ambler and Roy L. Crole
Mark Staples
Klaus Schneider and Dirk W. Hoffmann
Bernd Grobauer and Olaf Müller
Dominique Bolignano
Haiyan Xiong, Paul Curzon and Sofiène Tahar
Joe Hurd
Mark D. Aagaard, Robert B. Jones and Carl-Johan H. Seger
Nancy A. Day and Jeffrey J. Joyce
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