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

TOTAL DOCUMENTS

23

(FIVE YEARS 0)

H-INDEX

10

(FIVE YEARS 0)

Published By Springer Berlin Heidelberg

9783540406648, 9783540451303

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

Verified Bytecode Subroutines

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

10.1007/10930755_4 ◽

2003 ◽

pp. 55-70 ◽

Author(s):

Gerwin Klein ◽

Martin Wildmoser

Download Full-text

Formalizing Hilbert’s Grundlagen in Isabelle/Isar

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

10.1007/10930755_21 ◽

2003 ◽

pp. 319-334 ◽

Author(s):

Laura I. Meikle ◽

Jacques D. Fleuriot

Download Full-text

MetaPRL – A Modular Logical Environment

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

10.1007/10930755_19 ◽

2003 ◽

pp. 287-303 ◽

Author(s):

Jason Hickey ◽

Aleksey Nogin ◽

Robert L. Constable ◽

Brian E. Aydemir ◽

Eli Barzilay ◽

...

Download Full-text

Implementing Modules in the Coq System

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

10.1007/10930755_18 ◽

2003 ◽

pp. 270-286 ◽

Author(s):

Jacek Chrząszcz

Download Full-text

Program Extraction from Large Proof Developments

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

10.1007/10930755_14 ◽

2003 ◽

pp. 205-220 ◽

Author(s):

Luís Cruz-Filipe ◽

Bas Spitters

Keyword(s):

Program Extraction

Download Full-text

Proving Pearl: Knuth’s Algorithm for Prime Numbers

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

10.1007/10930755_20 ◽

2003 ◽

pp. 304-318 ◽

Author(s):

Laurent Théry

Keyword(s):

Download Full-text

Extending Higher-Order Unification to Support Proof Irrelevance

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

10.1007/10930755_16 ◽

2003 ◽

pp. 238-252 ◽

Author(s):

Jason Reed

Keyword(s):

Download Full-text

Inductive Invariants for Nested Recursion

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

10.1007/10930755_17 ◽

2003 ◽

pp. 253-269 ◽

Author(s):

Sava Krstić ◽

John Matthews

Keyword(s):

Nested Recursion ◽

Inductive Invariants

Download Full-text

Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover

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

10.1007/10930755_11 ◽

2003 ◽

pp. 171-187 ◽

Author(s):

Hasan Amjad

Keyword(s):

Theorem Prover ◽

Model Checker ◽

Download Full-text

Click’n Prove: Interactive Proofs within Set Theory

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

10.1007/10930755_1 ◽

2003 ◽

pp. 1-24 ◽

Author(s):

Jean-Raymond Abrial ◽

Dominique Cansell

Keyword(s):

Interactive Proofs

Download Full-text