@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",
}