scientific article; zbMATH DE number 3548474

zbMATH Open0352.68105MaRDI QIDQ4122841FDOQ4122841

Authors: L. S. van Benthem Jutting 

Publication date: 1977

Title of this publication is not available (Why is that?)

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)

• 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)