Some lambda calculus and type theory formalized
type: Item
instance of: scholarly article
title: Some lambda calculus and type theory formalized
zbMATH Open document ID: 0940.03019
DOI: 10.1023/A:1006294005493
author: James McKinna
author: Robert Pollack
published in: Journal of Automated Reasoning
publication date: 2000-01-30T00:00:00Z
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 1394794
zbMATH Keywords: formal mathematics
zbMATH Keywords: LEGO proof checker
zbMATH Keywords: pure type systems
zbMATH Keywords: survey
zbMATH Keywords: lambda calculus
zbMATH Keywords: constructive type theory
zbMATH Keywords: standardization for beta reduction
zbMATH Keywords: formal definitions
zbMATH Keywords: formal proof
describes a project that uses: Coq
describes a project that uses: Automath
describes a project that uses: LEGO
MaRDI profile type: Publication
Recommended article: Q3795649
Recommended article: A typed, algebraic, computational lambda-calculus
Recommended article: A unified approach to type theory through a refined \(\lambda\)-calculus
Recommended article: Q4263831
Recommended article: Q3714051
Recommended article: A typed lambda calculus with intersection types
Recommended article: Q3138540
Recommended article: Q4856946
Recommended article: Types for Proofs and Programs
Recommended article: Q4038654
description: scientific article; zbMATH DE number 1394794