scientific article; zbMATH DE number 3548474

MaRDI QIDQ4122841zbMATH OpenFDO

Authors L. S. van Benthem Jutting

Publication date 1977

Mathematics Subject Classification ID

General logic (03B99) Recursive ordinals and ordinal notations (03F15) 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)

Cited in

(21)

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

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)