Normal view MARC view ISBD view

Theorem Proving in Higher Order Logics [electronic resource] : 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings / edited by Joe Hurd, Tom Melham.

Contributor(s): Hurd, Joe [editor.] | Melham, Tom [editor.] | SpringerLink (Online service).
Material type: materialTypeLabelBookSeries: Theoretical Computer Science and General Issues: 3603Publisher: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2005Edition: 1st ed. 2005.Description: X, 414 p. online resource.Content type: text Media type: computer Carrier type: online resourceISBN: 9783540318200.Subject(s): Computer science | Computer systems | Machine theory | Software engineering | Artificial intelligence | Theory of Computation | Computer System Implementation | Formal Languages and Automata Theory | Computer Science Logic and Foundations of Programming | Software Engineering | Artificial IntelligenceAdditional physical formats: Printed edition:: No title; Printed edition:: No titleDDC classification: 004.0151 Online resources: Click here to access online
Contents:
Invited Papers -- On the Correctness of Operating System Kernels -- Alpha-Structural Recursion and Induction -- Regular Papers -- Shallow Lazy Proofs -- Mechanized Metatheory for the Masses: The PoplMark Challenge -- A Structured Set of Higher-Order Problems -- Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS -- Proving Equalities in a Commutative Ring Done Right in Coq -- A HOL Theory of Euclidean Space -- A Design Structure for Higher Order Quotients -- Axiomatic Constructor Classes in Isabelle/HOLCF -- Meta Reasoning in ACL2 -- Reasoning About Java Programs with Aliasing and Frame Conditions -- Real Number Calculations and Theorem Proving -- Verifying a Secure Information Flow Analyzer -- Proving Bounds for Real Linear Programs in Isabelle/HOL -- Essential Incompleteness of Arithmetic Verified by Coq -- Verification of BDD Normalization -- Extensionality in the Calculus of Constructions -- A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic -- A Generic Network on Chip Model -- Formal Verification of a SHA-1 Circuit Core Using ACL2 -- From PSL to LTL: A Formal Validation in HOL -- Proof Pearls -- Proof Pearl: A Formal Proof of Higman's Lemma in ACL2 -- Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2 -- Proof Pearl: Defining Functions over Finite Sets -- Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof.
In: Springer Nature eBookSummary: This volume constitutes the proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), which was held during22-25August2005inOxford,UK.TPHOLscoversallaspectsoftheorem proving in higher order logics as well as related topics in theorem proving and veri?cation. There were 49 papers submitted to TPHOLs 2005 in the full research c- egory, each of which was refereed by at least three reviewers selected by the programcommittee. Of these submissions, 20 researchpapersand 4 proof pearls were accepted for presentation at the conference and publication in this volume. In keeping with longstanding tradition, TPHOLs 2005 also o?ered a venue for the presentation of work in progress, where researchers invited discussion by means of a brief introductory talk and then discussed their work at a poster session. A supplementary proceedings volume was published as a 2005 technical report of the Oxford University Computing Laboratory. The organizers are grateful to Wolfgang Paul and Andrew Pitts for agreeing to give invited talks at TPHOLs 2005.
    average rating: 0.0 (0 votes)
No physical items for this record

Invited Papers -- On the Correctness of Operating System Kernels -- Alpha-Structural Recursion and Induction -- Regular Papers -- Shallow Lazy Proofs -- Mechanized Metatheory for the Masses: The PoplMark Challenge -- A Structured Set of Higher-Order Problems -- Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS -- Proving Equalities in a Commutative Ring Done Right in Coq -- A HOL Theory of Euclidean Space -- A Design Structure for Higher Order Quotients -- Axiomatic Constructor Classes in Isabelle/HOLCF -- Meta Reasoning in ACL2 -- Reasoning About Java Programs with Aliasing and Frame Conditions -- Real Number Calculations and Theorem Proving -- Verifying a Secure Information Flow Analyzer -- Proving Bounds for Real Linear Programs in Isabelle/HOL -- Essential Incompleteness of Arithmetic Verified by Coq -- Verification of BDD Normalization -- Extensionality in the Calculus of Constructions -- A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic -- A Generic Network on Chip Model -- Formal Verification of a SHA-1 Circuit Core Using ACL2 -- From PSL to LTL: A Formal Validation in HOL -- Proof Pearls -- Proof Pearl: A Formal Proof of Higman's Lemma in ACL2 -- Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2 -- Proof Pearl: Defining Functions over Finite Sets -- Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof.

This volume constitutes the proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), which was held during22-25August2005inOxford,UK.TPHOLscoversallaspectsoftheorem proving in higher order logics as well as related topics in theorem proving and veri?cation. There were 49 papers submitted to TPHOLs 2005 in the full research c- egory, each of which was refereed by at least three reviewers selected by the programcommittee. Of these submissions, 20 researchpapersand 4 proof pearls were accepted for presentation at the conference and publication in this volume. In keeping with longstanding tradition, TPHOLs 2005 also o?ered a venue for the presentation of work in progress, where researchers invited discussion by means of a brief introductory talk and then discussed their work at a poster session. A supplementary proceedings volume was published as a 2005 technical report of the Oxford University Computing Laboratory. The organizers are grateful to Wolfgang Paul and Andrew Pitts for agreeing to give invited talks at TPHOLs 2005.

There are no comments for this item.

Log in to your account to post a comment.