Lecture Notes in Computer Science - Theorem Proving in Higher Order Logics
Latest Publications

TOTAL DOCUMENTS

23

(FIVE YEARS 0)

H-INDEX

8

(FIVE YEARS 0)

Published By Springer Berlin Heidelberg

9783540230175, 9783540301424

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

Term Algebras with Length Function and Bounded Quantifier Alternation

Lecture Notes in Computer Science - Theorem Proving in Higher Order Logics ◽

10.1007/978-3-540-30142-4_23 ◽

2004 ◽

pp. 321-336 ◽

Author(s):

Ting Zhang ◽

Henny B. Sipma ◽

Zohar Manna

Keyword(s):

Length Function ◽

Quantifier Alternation

Download Full-text

Java Program Verification via a JVM Deep Embedding in ACL2

Lecture Notes in Computer Science - Theorem Proving in Higher Order Logics ◽

10.1007/978-3-540-30142-4_14 ◽

2004 ◽

pp. 184-200 ◽

Author(s):

Hanbing Liu ◽

J. Strother Moore

Keyword(s):

Program Verification ◽

Deep Embedding ◽

Download Full-text

Abstractions for Fault-Tolerant Distributed System Verification

Lecture Notes in Computer Science - Theorem Proving in Higher Order Logics ◽

10.1007/978-3-540-30142-4_19 ◽

2004 ◽

pp. 257-270 ◽

Author(s):

Lee Pike ◽

Jeffrey Maddalon ◽

Paul Miner ◽

Alfons Geser

Keyword(s):

Distributed System ◽

Fault Tolerant ◽

System Verification

Download Full-text

Certifying Machine Code Safety: Shallow Versus Deep Embedding

Lecture Notes in Computer Science - Theorem Proving in Higher Order Logics ◽

10.1007/978-3-540-30142-4_22 ◽

2004 ◽

pp. 305-320 ◽

Author(s):

Martin Wildmoser ◽

Tobias Nipkow

Keyword(s):

Machine Code ◽

Download Full-text

Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code

Lecture Notes in Computer Science - Theorem Proving in Higher Order Logics ◽

10.1007/978-3-540-30142-4_10 ◽

2004 ◽

pp. 118-135 ◽

Author(s):

Nadeem Abdul Hamid ◽

Zhong Shao

Keyword(s):

Type Systems ◽

Download Full-text

Higher Order Rippling in IsaPlanner

Lecture Notes in Computer Science - Theorem Proving in Higher Order Logics ◽

10.1007/978-3-540-30142-4_7 ◽

2004 ◽

pp. 83-98 ◽

Author(s):

Lucas Dixon ◽

Jacques Fleuriot

Keyword(s):

Download Full-text

Formalizing Integration Theory with an Application to Probabilistic Algorithms

Lecture Notes in Computer Science - Theorem Proving in Higher Order Logics ◽

10.1007/978-3-540-30142-4_20 ◽

2004 ◽

pp. 271-286 ◽

Author(s):

Stefan Richter

Keyword(s):

Integration Theory ◽

Probabilistic Algorithms

Download Full-text

A Decision Procedure for Geometry in Coq

Lecture Notes in Computer Science - Theorem Proving in Higher Order Logics ◽

10.1007/978-3-540-30142-4_17 ◽

2004 ◽

pp. 225-240 ◽

Author(s):

Julien Narboux

Keyword(s):

Decision Procedure

Download Full-text

Formalizing the Proof of the Kepler Conjecture

Lecture Notes in Computer Science - Theorem Proving in Higher Order Logics ◽

10.1007/978-3-540-30142-4_9 ◽

2004 ◽

pp. 117-117 ◽

Author(s):

Thomas Hales

Keyword(s):

Kepler Conjecture

Download Full-text

A Mechanical Proof of the Cook-Levin Theorem

Lecture Notes in Computer Science - Theorem Proving in Higher Order Logics ◽

10.1007/978-3-540-30142-4_8 ◽

2004 ◽

pp. 99-116 ◽

Author(s):

Ruben Gamboa ◽

John Cowles

Keyword(s):

Mechanical Proof

Download Full-text