scientific article
From MaRDI portal
Publication:4012882
zbMath0754.03041MaRDI QIDQ4012882
Publication date: 27 September 1992
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Logic in computer science (03B70) Second- and higher-order arithmetic and fragments (03F35) Combinatory logic and lambda calculus (03B40)
Related Items (24)
Formal metatheory of the lambda calculus using Stoughton's substitution ⋮ Types for modules ⋮ A note on the proof theory of the \(\lambda \Pi\)-calculus ⋮ Higher-order superposition for dependent types ⋮ Categorical reconstruction of a reduction free normalization proof ⋮ Formalizing adequacy: a case study for higher-order abstract syntax ⋮ Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters ⋮ The metatheory of UTT ⋮ The Alf proof editor and its proof engine ⋮ Closure under alpha-conversion ⋮ Canonicity and normalization for dependent type theory ⋮ A linear logical framework ⋮ Typed operational semantics for higher-order subtyping. ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A typed \(\lambda\)-calculus for proving-by-example and bottom-up generalization procedure ⋮ An algorithm for checking incomplete proof objects in type theory with localization and unification ⋮ Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus ⋮ Dependent Types at Work ⋮ Unnamed Item ⋮ Type inference for pure type systems ⋮ An adequacy theorem for dependent type theory ⋮ A Representation of Fω in LF ⋮ A Meta Linear Logical Framework
This page was built for publication:
