1 option
Theorem Proving in Higher Order Logics : 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. Proceedings / edited by Victor A. Carreno, Cesar A. Munoz, Sofiene Tahar.
LIBRA Q341 .P7 2004
Available from offsite location
- Format:
- Book
- Series:
- Computer Science (Springer-11645)
- Lecture notes in computer science 0302-9743 ; 2410.
- Lecture Notes in Computer Science, 0302-9743 ; 2410
- Language:
- English
- Subjects (All):
- Computer architecture.
- Computers.
- Software engineering.
- Logic design.
- Computer System Implementation.
- Theory of Computation.
- Software Engineering.
- Logic Design.
- Local Subjects:
- Computer System Implementation.
- Theory of Computation.
- Software Engineering.
- Logic Design.
- Physical Description:
- 1 online resource (X, 347 pages).
- Edition:
- First edition 2002.
- Contained In:
- Springer eBooks
- Place of Publication:
- Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2002.
- System Details:
- text file PDF
- Contents:
- 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.
- Other Format:
- Printed edition:
- ISBN:
- 978-3-540-45685-8
- 9783540456858
- Access Restriction:
- Restricted for use by site license.
The Penn Libraries is committed to describing library materials using current, accurate, and responsible language. If you discover outdated or inaccurate language, please fill out this feedback form to report it and suggest alternative language.