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 (18)
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
This page was built for publication:
