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

TOTAL DOCUMENTS

28

(FIVE YEARS 0)

H-INDEX

10

(FIVE YEARS 0)

Published By Springer Berlin Heidelberg

9783540615873, 9783540706410

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

A modular coding of UNITY in COQ

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

10.1007/bfb0105409 ◽

1996 ◽

pp. 251-266 ◽

Author(s):

Barbara Heyd ◽

Pierre Crégut

Download Full-text

Proving liveness of fair transition systems

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

10.1007/bfb0105398 ◽

1996 ◽

pp. 77-92

Author(s):

Holger Busch

Keyword(s):

Transition Systems

Download Full-text

A mechanisation of computability theory in HOL

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

10.1007/bfb0105420 ◽

1996 ◽

pp. 431-446 ◽

Author(s):

Vincent Zammit

Keyword(s):

Computability Theory

Download Full-text

Synthetic domain theory in type theory: Another logic of computable functions

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

10.1007/bfb0105416 ◽

1996 ◽

pp. 363-380 ◽

Author(s):

Bernhard Reus

Keyword(s):

Type Theory ◽

Domain Theory ◽

Computable Functions

Download Full-text

Inference rules for programming languages with side effects in expressions

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

10.1007/bfb0105396 ◽

1996 ◽

pp. 51-60 ◽

Author(s):

Paul E. Black ◽

Phillip J. Windley

Keyword(s):

Side Effects ◽

Programming Languages ◽

Inference Rules

Download Full-text

Elements of mathematical analysis in PVS

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

10.1007/bfb0105402 ◽

1996 ◽

pp. 141-156 ◽

Author(s):

Bruno Dutertre

Keyword(s):

Mathematical Analysis

Download Full-text

Towards applying the composition principle to verify a microkernel operating system

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

10.1007/bfb0105408 ◽

1996 ◽

pp. 235-250 ◽

Author(s):

Mark R. Heckman ◽

Cui Zhang ◽

Brian R. Becker ◽

Dave Peticolas ◽

Karl N. Levitt ◽

...

Keyword(s):

Operating System

Download Full-text

Translating specifications in VDM-SL to PVS

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

10.1007/bfb0105393 ◽

1996 ◽

pp. 1-16 ◽

Author(s):

Sten Agerholm

Download Full-text

A comparison of HOL and ALF formalizations of a categorical coherence theorem

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

10.1007/bfb0105394 ◽

1996 ◽

pp. 17-32 ◽

Author(s):

Sten Agerholm ◽

Ilya Beylin ◽

Peter Dybjer

Keyword(s):

Coherence Theorem

Download Full-text

Verification of compiler correctness for the WAM

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

10.1007/bfb0105415 ◽

1996 ◽

pp. 347-361 ◽

Author(s):

Cornelia Pusch

Keyword(s):

Compiler Correctness

Download Full-text