|
|
|
|
| LEADER |
02532nmm a2200361 u 4500 |
| 001 |
EB001884279 |
| 003 |
EBX01000000000000001047646 |
| 005 |
00000000000000.0 |
| 007 |
cr||||||||||||||||||||| |
| 008 |
191115 ||| eng |
| 020 |
|
|
|a 9783540456858
|
| 100 |
1 |
|
|a Carreno, Victor A.
|e [editor]
|
| 245 |
0 |
0 |
|a Theorem Proving in Higher Order Logics
|h Elektronische Ressource
|b 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings
|c edited by Victor A. Carreno, Cesar A. Munoz, Sofiene Tahar
|
| 250 |
|
|
|a 1st ed. 2002
|
| 260 |
|
|
|a Berlin, Heidelberg
|b Springer Berlin Heidelberg
|c 2002, 2002
|
| 300 |
|
|
|a X, 347 p
|b online resource
|
| 505 |
0 |
|
|a 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
|
| 653 |
|
|
|a Computer systems
|
| 653 |
|
|
|a Software engineering
|
| 653 |
|
|
|a Computer science
|
| 653 |
|
|
|a Computer System Implementation
|
| 653 |
|
|
|a Software Engineering
|
| 653 |
|
|
|a Logic design
|
| 653 |
|
|
|a Logic Design
|
| 653 |
|
|
|a Theory of Computation
|
| 700 |
1 |
|
|a Munoz, Cesar A.
|e [editor]
|
| 700 |
1 |
|
|a Tahar, Sofiene
|e [editor]
|
| 041 |
0 |
7 |
|a eng
|2 ISO 639-2
|
| 989 |
|
|
|b SBA
|a Springer Book Archives -2004
|
| 490 |
0 |
|
|a Lecture Notes in Computer Science
|
| 028 |
5 |
0 |
|a 10.1007/3-540-45685-6
|
| 856 |
4 |
0 |
|u https://doi.org/10.1007/3-540-45685-6?nosfx=y
|x Verlag
|3 Volltext
|
| 082 |
0 |
|
|a 004.2
|