Theorem Proving in Higher Order Logics 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings /
| Συγγραφή απο Οργανισμό/Αρχή: | |
|---|---|
| Άλλοι συγγραφείς: | , , |
| Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
| Γλώσσα: | English |
| Έκδοση: |
Berlin, Heidelberg :
Springer Berlin Heidelberg : Imprint: Springer,
2002.
|
| Έκδοση: | 1st ed. 2002. |
| Σειρά: | Lecture Notes in Computer Science,
2410 |
| Θέματα: | |
| Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- 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.
