scientific article; zbMATH DE number 3548474
From MaRDI portal
Publication:4122841
zbMATH Open0352.68105MaRDI QIDQ4122841FDOQ4122841
Publication date: 1977
Title of this publication is not available (Why is that?)
Research exposition (monographs, survey articles) pertaining to computer science (68-02) General topics in the theory of software (68N01) Symbolic computation and algebraic computation (68W30) Recursive ordinals and ordinal notations (03F15) General logic (03B99)
Cited In (18)
- Winskel is (almost) right. Towards a mechanized semantics textbook
- A unified approach to type theory through a refined \(\lambda\)-calculus
- A certified, corecursive implementation of exact real numbers
- The foundation of a generic theorem prover
- On preserving the computational content of mathematical proofs: toy examples for a formalising strategy
- Formalising Mathematics in Simple Type Theory
- Computer theorem proving in mathematics
- A short proof of the strong normalization of classical natural deduction with disjunction
- Automath
- Applications of real number theorem proving in PVS
- N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker
- Formalizing Ordinal Partition Relations Using Isabelle/HOL
- Computational logic: its origins and applications
- Exploring the structure of an algebra text with locales
- Using typed lambda calculus to implement formal systems on a machine
- Constructing the real numbers in HOL
- Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project
- The practice of logical frameworks
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4122841)
