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

TOTAL DOCUMENTS

(FIVE YEARS 0)

H-INDEX

(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 ◽

Cited By ~ 5

Author(s):

Ting Zhang ◽

Henny B. Sipma ◽

Zohar Manna

Keyword(s):

Length Function ◽

Quantifier Alternation

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 ◽

Cited By ~ 15

Author(s):

Hanbing Liu ◽

J. Strother Moore

Keyword(s):

Program Verification ◽

Deep Embedding ◽

Java Program

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 ◽

Cited By ~ 14

Author(s):

Lee Pike ◽

Jeffrey Maddalon ◽

Paul Miner ◽

Alfons Geser

Keyword(s):

Distributed System ◽

Fault Tolerant ◽

System Verification

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 ◽

Cited By ~ 14

Author(s):

Lucas Dixon ◽

Jacques Fleuriot

Keyword(s):

Higher Order

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 ◽

Cited By ~ 11

Author(s):

Stefan Richter

Keyword(s):

Integration Theory ◽

Probabilistic Algorithms

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 ◽

Cited By ~ 28

Author(s):

Martin Wildmoser ◽

Tobias Nipkow

Keyword(s):

Machine Code ◽

Deep Embedding

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 ◽

Cited By ~ 7

Author(s):

Nadeem Abdul Hamid ◽

Zhong Shao

Keyword(s):

Type Systems ◽

Hoare Logic

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 ◽

Cited By ~ 15

Author(s):

Julien Narboux

Keyword(s):

Decision Procedure

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 ◽

Cited By ~ 3

Author(s):

Thomas Hales

Keyword(s):

Kepler Conjecture

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 ◽

Cited By ~ 1

Author(s):

Ruben Gamboa ◽

John Cowles

Keyword(s):

Mechanical Proof

Lecture Notes in Computer Science - Theorem Proving in Higher Order LogicsLatest Publications

TOTAL DOCUMENTS

H-INDEX

Published By Springer Berlin Heidelberg

Term Algebras with Length Function and Bounded Quantifier Alternation

Java Program Verification via a JVM Deep Embedding in ACL2

Abstractions for Fault-Tolerant Distributed System Verification

Higher Order Rippling in IsaPlanner

Formalizing Integration Theory with an Application to Probabilistic Algorithms

Certifying Machine Code Safety: Shallow Versus Deep Embedding

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

A Decision Procedure for Geometry in Coq

Formalizing the Proof of the Kepler Conjecture

A Mechanical Proof of the Cook-Levin Theorem

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