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

TOTAL DOCUMENTS

25

(FIVE YEARS 0)

H-INDEX

10

(FIVE YEARS 0)

Published By Springer Berlin Heidelberg

9783540710653, 9783540710677

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

A Brief Overview of PVS

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

10.1007/978-3-540-71067-7_5 ◽

2008 ◽

pp. 22-27 ◽

Author(s):

Sam Owre ◽

Natarajan Shankar

Download Full-text

An ACL2 Tutorial

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

10.1007/978-3-540-71067-7_4 ◽

2008 ◽

pp. 17-21 ◽

Author(s):

Matt Kaufmann ◽

J Strother Moore

Download Full-text

Formalizing Soundness of Contextual Effects

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

10.1007/978-3-540-71067-7_22 ◽

2008 ◽

pp. 262-277 ◽

Author(s):

Polyvios Pratikakis ◽

Jeffrey S. Foster ◽

Michael Hicks ◽

Iulian Neamtiu

Keyword(s):

Contextual Effects

Download Full-text

Will This Be Formal?

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

10.1007/978-3-540-71067-7_2 ◽

2008 ◽

pp. 6-11 ◽

Author(s):

Steven P. Miller

Download Full-text

Proof Pearl: Revisiting the Mini-rubik in Coq

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

10.1007/978-3-540-71067-7_25 ◽

2008 ◽

pp. 310-319 ◽

Author(s):

Laurent Théry

Download Full-text

Secure Microkernels, State Monads and Scalable Refinement

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

10.1007/978-3-540-71067-7_16 ◽

2008 ◽

pp. 167-182 ◽

Author(s):

David Cock ◽

Gerwin Klein ◽

Thomas Sewell

Download Full-text

A Formalized Theory for Verifying Stability and Convergence of Automata in PVS

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

10.1007/978-3-540-71067-7_20 ◽

2008 ◽

pp. 230-245 ◽

Author(s):

Sayan Mitra ◽

K. Mani Chandy

Keyword(s):

Stability And Convergence

Download Full-text

Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL

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

10.1007/978-3-540-71067-7_24 ◽

2008 ◽

pp. 294-309 ◽

Author(s):

Daniel Wasserrab ◽

Andreas Lochbihler

Keyword(s):

Dynamic Slicing ◽

Dependence Graphs ◽

Program Dependence

Download Full-text

A Brief Overview of HOL4

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

10.1007/978-3-540-71067-7_6 ◽

2008 ◽

pp. 28-32 ◽

Author(s):

Konrad Slind ◽

Michael Norrish

Download Full-text

A Short Presentation of Coq

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

10.1007/978-3-540-71067-7_3 ◽

2008 ◽

pp. 12-16 ◽

Author(s):

Yves Bertot

Keyword(s):

Short Presentation

Download Full-text