E-Book, Englisch, Band 2410, 347 Seiten, eBook
Carreno / Munoz / Tahar Theorem Proving in Higher Order Logics
2002
ISBN: 978-3-540-45685-8
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark
15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings
E-Book, Englisch, Band 2410, 347 Seiten, eBook
Reihe: Lecture Notes in Computer Science
ISBN: 978-3-540-45685-8
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark
Zielgruppe
Research
Autoren/Hrsg.
Weitere Infos & Material
Invited Talks.- Formal Methods at NASA Langley.- Higher Order Unification 30 Years Later.- Regular Papers.- Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction.- Efficient Reasoning about Executable Specifications in Coq.- Verified Bytecode Model Checkers.- The 5 Colour Theorem in Isabelle/Isar.- Type-Theoretic Functional Semantics.- A Proposal for a Formal OCL Semantics in Isabelle/HOL.- Explicit Universes for the Calculus of Constructions.- Formalised Cut Admissibility for Display Logic.- Formalizing the Trading Theorem for the Classification of Surfaces.- Free-Style Theorem Proving.- A Comparison of Two Proof Critics: Power vs. Robustness.- Two-Level Meta-reasoning in Coq.- PuzzleTool: An Example of Programming Computation and Deduction.- A Formal Approach to Probabilistic Termination.- Using Theorem Proving for Numerical Analysis Correctness Proof of an Automatic Differentiation Algorithm.- Quotient Types: A Modular Approach.- Sequent Schema for Derived Rules.- Algebraic Structures and Dependent Records.- Proving the Equivalence of Microstep and Macrostep Semantics.- Weakest Precondition for General Recursive Programs Formalized in Coq.
