Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
  • 1
    UID:
    gbv_393023583
    Format: VIII, 336 S. , graph. Darst. , 235 mm x 155 mm
    ISBN: 3540230173
    Series Statement: Lecture notes in computer science 3223
    Note: Literaturangaben
    Additional Edition: Erscheint auch als Online-Ausgabe Slind, Konrad Theorem Proving in Higher Order Logics Berlin, Heidelberg : Springer Berlin Heidelberg, 2004 ISBN 9783540230175
    Language: English
    Subjects: Computer Science
    RVK:
    Keywords: Automatisches Beweisverfahren ; HOL ; Formale Sprache ; Deduktion ; Automatisches Beweisverfahren ; Programmverifikation ; Logischer Entwurf ; Konferenzschrift ; Kongress ; Konferenzschrift
    URL: Cover
    URL: Volltext  (Online Access)
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 2
    UID:
    almahu_9947920709802882
    Format: VIII, 340 p. , online resource.
    ISBN: 9783540301424
    Series Statement: Lecture Notes in Computer Science, 3223
    Content: This volume constitutes the proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004) held September 14–17, 2004 in Park City, Utah, USA. TPHOLs covers all aspects of theorem proving in higher-order logics as well as related topics in theorem proving and veri?cation. There were 42 papers submitted to TPHOLs 2004 in the full research ca- gory, each of which was refereed by at least 3 reviewers selected by the program committee. Of these submissions, 21 were accepted for presentation at the c- ference and publication in this volume. In keeping with longstanding tradition, TPHOLs 2004 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 c- taining papers about in-progress work was published as a 2004 technical report of the School of Computing at the University of Utah. The organizers are grateful to Al Davis, Thomas Hales, and Ken McMillan for agreeing to give invited talks at TPHOLs 2004. The TPHOLs conference traditionally changes continents each year in order to maximize the chances that researchers from around the world can attend.
    Note: Error Analysis of Digital Filters Using Theorem Proving -- Verifying Uniqueness in a Logical Framework -- A Program Logic for Resource Verification -- Proof Reuse with Extended Inductive Types -- Hierarchical Reflection -- Correct Embedded Computing Futures -- Higher Order Rippling in IsaPlanner -- A Mechanical Proof of the Cook-Levin Theorem -- Formalizing the Proof of the Kepler Conjecture -- Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code -- Extensible Hierarchical Tactic Construction in a Logical Framework -- Theorem Reuse by Proof Term Transformation -- Proving Compatibility Using Refinement -- Java Program Verification via a JVM Deep Embedding in ACL2 -- Reasoning About CBV Functional Programs in Isabelle/HOL -- Proof Pearl: From Concrete to Functional Unparsing -- A Decision Procedure for Geometry in Coq -- Recursive Function Definition for Types with Binders -- Abstractions for Fault-Tolerant Distributed System Verification -- Formalizing Integration Theory with an Application to Probabilistic Algorithms -- Formalizing Java Dynamic Loading in HOL -- Certifying Machine Code Safety: Shallow Versus Deep Embedding -- Term Algebras with Length Function and Bounded Quantifier Alternation.
    In: Springer eBooks
    Additional Edition: Printed edition: ISBN 9783540230175
    Language: English
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 3
    UID:
    gbv_749271167
    Format: Online-Ressource (VIII, 337 p. Also available online) , digital
    Edition: Springer eBook Collection. Computer Science
    ISBN: 9783540301424 , 3540230173 , 9783540230175
    Series Statement: Lecture Notes in Computer Science 3223
    Content: This book constitutes the refereed proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2004, held in Park City, Utah, USA, in September 2004. The 21 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 42 submissions. Among the topics addressed are theorem proving, verification, inductive types, automated deduction, mechanized proofs, mathematical logic, proof theory, type systems, computability, program verification, ACL, Cop, Isabelle/HOL, recursive functions, integration theory, machine code safety certification, and abstraction
    Note: Literaturangaben
    Additional Edition: ISBN 9783540230175
    Additional Edition: Erscheint auch als Druck-Ausgabe ISBN 9783662211625
    Additional Edition: Erscheint auch als Druck-Ausgabe ISBN 9783540230175
    Language: English
    Subjects: Computer Science
    RVK:
    Keywords: Automatisches Beweisverfahren ; HOL ; Formale Sprache ; Deduktion ; Automatisches Beweisverfahren ; Programmverifikation ; Logischer Entwurf ; Konferenzschrift
    URL: Volltext  (lizenzpflichtig)
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
  • 4
    UID:
    almahu_9948621687502882
    Format: VIII, 340 p. , online resource.
    Edition: 1st ed. 2004.
    ISBN: 9783540301424
    Series Statement: Lecture Notes in Computer Science, 3223
    Content: This volume constitutes the proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2004) held September 14-17, 2004 in Park City, Utah, USA. TPHOLs covers all aspects of theorem proving in higher-order logics as well as related topics in theorem proving and veri?cation. There were 42 papers submitted to TPHOLs 2004 in the full research ca- gory, each of which was refereed by at least 3 reviewers selected by the program committee. Of these submissions, 21 were accepted for presentation at the c- ference and publication in this volume. In keeping with longstanding tradition, TPHOLs 2004 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 c- taining papers about in-progress work was published as a 2004 technical report of the School of Computing at the University of Utah. The organizers are grateful to Al Davis, Thomas Hales, and Ken McMillan for agreeing to give invited talks at TPHOLs 2004. The TPHOLs conference traditionally changes continents each year in order to maximize the chances that researchers from around the world can attend.
    Note: Error Analysis of Digital Filters Using Theorem Proving -- Verifying Uniqueness in a Logical Framework -- A Program Logic for Resource Verification -- Proof Reuse with Extended Inductive Types -- Hierarchical Reflection -- Correct Embedded Computing Futures -- Higher Order Rippling in IsaPlanner -- A Mechanical Proof of the Cook-Levin Theorem -- Formalizing the Proof of the Kepler Conjecture -- Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code -- Extensible Hierarchical Tactic Construction in a Logical Framework -- Theorem Reuse by Proof Term Transformation -- Proving Compatibility Using Refinement -- Java Program Verification via a JVM Deep Embedding in ACL2 -- Reasoning About CBV Functional Programs in Isabelle/HOL -- Proof Pearl: From Concrete to Functional Unparsing -- A Decision Procedure for Geometry in Coq -- Recursive Function Definition for Types with Binders -- Abstractions for Fault-Tolerant Distributed System Verification -- Formalizing Integration Theory with an Application to Probabilistic Algorithms -- Formalizing Java Dynamic Loading in HOL -- Certifying Machine Code Safety: Shallow Versus Deep Embedding -- Term Algebras with Length Function and Bounded Quantifier Alternation.
    In: Springer Nature eBook
    Additional Edition: Printed edition: ISBN 9783662211625
    Additional Edition: Printed edition: ISBN 9783540230175
    Language: English
    Library Location Call Number Volume/Issue/Year Availability
    BibTip Others were also interested in ...
Did you mean 9783540201755?
Did you mean 9783504230975?
Did you mean 9783540200475?
Close ⊗
This website uses cookies and the analysis tool Matomo. Further information can be found on the KOBV privacy pages