Executing higher order logic

Stefan Berghofer; Tobias Nipkow

doi:10.1007/3-540-45842-5_2

Executing higher order logic

Stefan Berghofer, Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

Technical University of Munich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

65 Scopus citations

Abstract

We report on the design of a prototyping component for the theorem prover Isabelle/HOL. Specifications consisting of datatypes, recursive functions and inductive definitions are compiled into a functional program. Functions and inductively defined relations can be mixed. Inductive definitions must be such that they can be executed in Prolog style but requiring only matching rather than unification. This restriction is enforced by a mode analysis. Tail recursive partial functions can be defined and executed with the help of a while combinator.

Original language	English
Title of host publication	Types for Proofs and Programs - International Workshop, TYPES 2000, Selected Papers
Editors	Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack, Robert Pollack
Publisher	Springer Verlag
Pages	24-40
Number of pages	17
ISBN (Print)	3540432876, 9783540432876
DOIs	https://doi.org/10.1007/3-540-45842-5_2
State	Published - 2002
Event	1st Annual Workshop of the TYPES Working Group on Computer-Assisted Reasoning Based on Type Theory, TYPES 2000 - Durham, United Kingdom Duration: 8 Dec 2000 → 12 Dec 2000

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2277 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	1st Annual Workshop of the TYPES Working Group on Computer-Assisted Reasoning Based on Type Theory, TYPES 2000
Country/Territory	United Kingdom
City	Durham
Period	8/12/00 → 12/12/00

Access to Document

10.1007/3-540-45842-5_2

Cite this

Berghofer, S., & Nipkow, T. (2002). Executing higher order logic. In P. Callaghan, Z. Luo, J. McKinna, R. Pollack, & R. Pollack (Eds.), Types for Proofs and Programs - International Workshop, TYPES 2000, Selected Papers (pp. 24-40). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2277 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-45842-5_2

Berghofer, Stefan ; Nipkow, Tobias. / Executing higher order logic. Types for Proofs and Programs - International Workshop, TYPES 2000, Selected Papers. editor / Paul Callaghan ; Zhaohui Luo ; James McKinna ; Robert Pollack ; Robert Pollack. Springer Verlag, 2002. pp. 24-40 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{1db3471f4aba45be88e392fc3ad3c375,

title = "Executing higher order logic",

abstract = "We report on the design of a prototyping component for the theorem prover Isabelle/HOL. Specifications consisting of datatypes, recursive functions and inductive definitions are compiled into a functional program. Functions and inductively defined relations can be mixed. Inductive definitions must be such that they can be executed in Prolog style but requiring only matching rather than unification. This restriction is enforced by a mode analysis. Tail recursive partial functions can be defined and executed with the help of a while combinator.",

author = "Stefan Berghofer and Tobias Nipkow",

year = "2002",

doi = "10.1007/3-540-45842-5_2",

language = "English",

isbn = "3540432876",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "24--40",

editor = "Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack and Robert Pollack",

booktitle = "Types for Proofs and Programs - International Workshop, TYPES 2000, Selected Papers",

note = "1st Annual Workshop of the TYPES Working Group on Computer-Assisted Reasoning Based on Type Theory, TYPES 2000 ; Conference date: 08-12-2000 Through 12-12-2000",

}

Berghofer, S & Nipkow, T 2002, Executing higher order logic. in P Callaghan, Z Luo, J McKinna, R Pollack & R Pollack (eds), Types for Proofs and Programs - International Workshop, TYPES 2000, Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2277 LNCS, Springer Verlag, pp. 24-40, 1st Annual Workshop of the TYPES Working Group on Computer-Assisted Reasoning Based on Type Theory, TYPES 2000, Durham, United Kingdom, 8/12/00. https://doi.org/10.1007/3-540-45842-5_2

Executing higher order logic. / Berghofer, Stefan; Nipkow, Tobias.
Types for Proofs and Programs - International Workshop, TYPES 2000, Selected Papers. ed. / Paul Callaghan; Zhaohui Luo; James McKinna; Robert Pollack; Robert Pollack. Springer Verlag, 2002. p. 24-40 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2277 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Executing higher order logic

AU - Berghofer, Stefan

AU - Nipkow, Tobias

PY - 2002

Y1 - 2002

N2 - We report on the design of a prototyping component for the theorem prover Isabelle/HOL. Specifications consisting of datatypes, recursive functions and inductive definitions are compiled into a functional program. Functions and inductively defined relations can be mixed. Inductive definitions must be such that they can be executed in Prolog style but requiring only matching rather than unification. This restriction is enforced by a mode analysis. Tail recursive partial functions can be defined and executed with the help of a while combinator.

AB - We report on the design of a prototyping component for the theorem prover Isabelle/HOL. Specifications consisting of datatypes, recursive functions and inductive definitions are compiled into a functional program. Functions and inductively defined relations can be mixed. Inductive definitions must be such that they can be executed in Prolog style but requiring only matching rather than unification. This restriction is enforced by a mode analysis. Tail recursive partial functions can be defined and executed with the help of a while combinator.

UR - http://www.scopus.com/inward/record.url?scp=84874828803&partnerID=8YFLogxK

U2 - 10.1007/3-540-45842-5_2

DO - 10.1007/3-540-45842-5_2

M3 - Conference contribution

AN - SCOPUS:84874828803

SN - 3540432876

SN - 9783540432876

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 24

EP - 40

BT - Types for Proofs and Programs - International Workshop, TYPES 2000, Selected Papers

A2 - Callaghan, Paul

A2 - Luo, Zhaohui

A2 - McKinna, James

A2 - Pollack, Robert

PB - Springer Verlag

T2 - 1st Annual Workshop of the TYPES Working Group on Computer-Assisted Reasoning Based on Type Theory, TYPES 2000

Y2 - 8 December 2000 through 12 December 2000

ER -

Berghofer S, Nipkow T. Executing higher order logic. In Callaghan P, Luo Z, McKinna J, Pollack R, Pollack R, editors, Types for Proofs and Programs - International Workshop, TYPES 2000, Selected Papers. Springer Verlag. 2002. p. 24-40. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-45842-5_2

Executing higher order logic

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this