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

9783540633792, 9783540695264

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

A full formalisation of π-calculus theory in the calculus of constructions

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

10.1007/bfb0028392 ◽

1997 ◽

pp. 153-169 ◽

Cited By ~ 26

Author(s):

Daniel Hirschkoff

Keyword(s):

Calculus Of Constructions ◽

Π Calculus

Download Full-text

Towards an object-oriented progification language

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

10.1007/bfb0028396 ◽

1997 ◽

pp. 215-230 ◽

Cited By ~ 1

Author(s):

Wolfgang Naraschewski

Keyword(s):

Object Oriented

Download Full-text

Verifying the accuracy of polynomial approximations in HOL

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

10.1007/bfb0028391 ◽

1997 ◽

pp. 137-152 ◽

Cited By ~ 12

Author(s):

John Harrison

Keyword(s):

Polynomial Approximations

Download Full-text

Refining reactive systems in HOL using action systems

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

10.1007/bfb0028394 ◽

1997 ◽

pp. 183-197 ◽

Cited By ~ 3

Author(s):

Thomas Långbacka ◽

Joakim von Wright

Keyword(s):

Reactive Systems ◽

Action Systems

Download Full-text

Executing formal specifications by translation to higher order logic programming

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

10.1007/bfb0028383 ◽

1997 ◽

pp. 17-32 ◽

Cited By ~ 4

Author(s):

James H. Andrews

Keyword(s):

Logic Programming ◽

Higher Order ◽

Order Logic ◽

Formal Specifications ◽

Higher Order Logic

Download Full-text

Proof presentation for Isabelle

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

10.1007/bfb0028399 ◽

1997 ◽

pp. 259-274 ◽

Cited By ~ 6

Author(s):

Martin Simons

Keyword(s):

Proof Presentation

Download Full-text

Type classes and overloading in higher-order logic

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

10.1007/bfb0028402 ◽

1997 ◽

pp. 307-322 ◽

Cited By ~ 59

Author(s):

Markus Wenzel

Keyword(s):

Higher Order ◽

Order Logic ◽

Higher Order Logic ◽

Type Classes

Download Full-text

Rewriting, decision procedures and lemma speculation for automated hardware verification

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

10.1007/bfb0028393 ◽

1997 ◽

pp. 171-182 ◽

Cited By ~ 4

Author(s):

Deepak Kapur

Keyword(s):

Decision Procedures ◽

Hardware Verification

Download Full-text

ML programming in constructive type theory

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

10.1007/bfb0028387 ◽

1997 ◽

pp. 87-87

Author(s):

Robert L. Constable

Keyword(s):

Type Theory ◽

Constructive Type Theory ◽

Constructive Type

Download Full-text

Formal verification of concurrent programs in Lp and in Coq: A comparative analysis

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

10.1007/bfb0028386 ◽

1997 ◽

pp. 69-85 ◽

Cited By ~ 2

Author(s):

Boutheina Chetali ◽

Barbara Heyd

Keyword(s):

Comparative Analysis ◽

Formal Verification ◽

Concurrent Programs

Download Full-text

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

TOTAL DOCUMENTS

H-INDEX

Published By Springer Berlin Heidelberg

A full formalisation of π-calculus theory in the calculus of constructions

Towards an object-oriented progification language

Verifying the accuracy of polynomial approximations in HOL

Refining reactive systems in HOL using action systems

Executing formal specifications by translation to higher order logic programming

Proof presentation for Isabelle

Type classes and overloading in higher-order logic

Rewriting, decision procedures and lemma speculation for automated hardware verification

ML programming in constructive type theory

Formal verification of concurrent programs in Lp and in Coq: A comparative analysis

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