scientific article; zbMATH DE number 3548474
From MaRDI portal
Publication:4122841
zbMath0352.68105MaRDI QIDQ4122841
Publication date: 1977
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Symbolic computation and algebraic computation (68W30) Research exposition (monographs, survey articles) pertaining to computer science (68-02) General topics in the theory of software (68N01) Recursive ordinals and ordinal notations (03F15) General logic (03B99)
Related Items
Constructing the real numbers in HOL, A unified approach to type theory through a refined \(\lambda\)-calculus, Computational logic: its origins and applications, Formalizing Ordinal Partition Relations Using Isabelle/HOL, N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker, Formalising Mathematics in Simple Type Theory, Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project, Exploring the structure of an algebra text with locales, Applications of real number theorem proving in PVS, A short proof of the strong normalization of classical natural deduction with disjunction, Using typed lambda calculus to implement formal systems on a machine, Computer theorem proving in mathematics, Automath, 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, A certified, corecursive implementation of exact real numbers
