scientific article
From MaRDI portal
Publication:2751370
zbMath1005.03011MaRDI QIDQ2751370
Herman Geuvers, Hendrik Pieter Barendregt
Publication date: 4 December 2001
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
The challenge of computer mathematics, Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants, Characteristics of de Bruijn’s early proof checker Automath, N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker, Mtac: A monad for typed tactic programming in Coq, Unnamed Item, Primitive Floats in Coq, Classical \(F_{\omega}\), orthogonality and symmetric candidates, Cut Elimination in a Class of Sequent Calculi for Pure Type Systems, Computer theorem proving in mathematics, Introduction to Type Theory, Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician, N. G. de Bruijn's contribution to the formalization of mathematics, Local Theory Specifications in Isabelle/Isar, Proof assistants: history, ideas and future, A Framework for Defining Logical Frameworks, Machine-Checked Security Proofs of Cryptographic Signature Schemes, Inductive and Coinductive Components of Corecursive Functions in Coq
Uses Software
