scientific article; zbMATH DE number 3548474

MaRDI QIDQ4122841zbMATHFDO

Authors L. S. van Benthem Jutting

Publication date 1977

Mathematics Subject Classification ID

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)

• Formalizing ordinal partition relations using Isabelle/HOL
• Exploring the structure of an algebra text with locales
• Computer theorem proving in mathematics
• Applications of real number theorem proving in PVS
• The foundation of a generic theorem prover
• On preserving the computational content of mathematical proofs: toy examples for a formalising strategy
• The practice of logical frameworks
• N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker
• Formalising Mathematics in Simple Type Theory
• Automath
• A certified, corecursive implementation of exact real numbers
• Using typed lambda calculus to implement formal systems on a machine
• Constructing the real numbers in HOL
• Computational logic: its origins and applications
• A short proof of the strong normalization of classical natural deduction with disjunction
• Winskel is (almost) right. Towards a mechanized semantics textbook
• A unified approach to type theory through a refined \(\lambda\)-calculus
• Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project

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)