scientific article; zbMATH DE number 1113859

zbMath0886.03008MaRDI QIDQ4375633

Douglas J. Howe

Publication date: 8 February 1998

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

constructive type theorysemanticsHOLNuprl

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Innovations in computational type theory using Nuprl ⋮ Validating Brouwer's continuity principle for numbers using named exceptions ⋮ MBase: Representing knowledge and context for the integration of mathematical software systems ⋮ Exercising Nuprl’s Open-Endedness ⋮ Hybrid interactive theorem proving using nuprl and HOL ⋮ Proof-search in type-theoretic languages: An introduction

Uses Software

• HOL
• Nuprl