scientific article; zbMATH DE number 2182489

zbMath1095.03017MaRDI QIDQ4681364

Thierry Coquand, Randy Pollack, Makoto Takeyama

Publication date: 23 June 2005

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

zbMATH Keywords

functional programming systemfoundational computer algebra systemMartin-Löf logical frameworkmodule-based systemstype-based proof (assistant) systemmeta-mathematical proof system

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Mechanization of proofs and logical operations (03B35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Second- and higher-order arithmetic and fragments (03F35) Combinatory logic and lambda calculus (03B40)

Related Items (4)

Working with Mathematical Structures in Type Theory ⋮ User interaction with the Matita proof assistant ⋮ A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance ⋮ Manifest Fields and Module Mechanisms in Intensional Type Theory

Uses Software

• Nuprl

This page was built for publication: