Logic for Computable Functions Description of a Machine Implementation
Abstract
The author uses the name LCF also for the logic itself, which is presented at the start of the paper, The proof-checking program is designed to allow the user interactively to generate formal proofs about computable functions and functionals over a variety of domains, including those of interest to the computer scientist - for example integers, lists and computer programs and their semantics.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 1972
- Accession Number
- AD0785072
Entities
People
- Robin Milner
Organizations
- Stanford University