Theorem Proving in Higher Order Logics : 15th International Conference, TPHOLs 2002 Hampton, VA, USA, August 20 23, 2002 Proceedings
Enregistré dans:
| Institution som forfatter: | |
|---|---|
| Andre forfattere: | , , |
| Format: | Livre numérique |
| Sprog: | Anglais |
| Udgivet: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Serier: | Lecture notes in computer science
2410 |
| Fag: | |
| Online adgang: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Kommentar: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Theorem proving in higher order logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, proceedings, Victor A. Carreño, César A. Muñoz, Sofiène Tahar, eds, Berlin, Springer, 2002, 1 vol. (X-347 p.), Lecture notes in computer science, 3-540-44039-9 • Theorem Proving in Higher Order Logics, Texte imprimé, 9783662182413 |
Indholdsfortegnelse:
- 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.