scientific article; zbMATH DE number 1948185

zbMath1020.03010MaRDI QIDQ4411846

Herman Geuvers, Gueorgui I. Jojgov

Publication date: 10 July 2003

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2471/24710537.htm

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

zbMATH Keywords

type theoryinteractive theorem provingopen termsmeta-variablesformulas-as-types

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

MikiBeta : A General GUI Library for Visualizing Proof Trees, Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms, Tactics and Parameters, Two-level Lambda-calculus, Implementing type theory in higher order constraint logic programming, A compact kernel for the calculus of inductive constructions, The lambda-context calculus (extended version), Tinycals: Step by Step Tacticals

Uses Software

• Automath
• ALF