scientific article; zbMATH DE number 512787

zbMath0835.68068MaRDI QIDQ4281480

James McKinna, Robert Pollack

Publication date: 1993

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

zbMATH Keywords

pure type systemsgeneralized type systems

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Related Items (22)

Types for modules ⋮ More Church-Rosser proofs (in Isabelle/HOL) ⋮ A canonical locally named representation of binding ⋮ Higher-order subtyping and its decidability ⋮ Finitary type theories with and without contexts ⋮ The metatheory of UTT ⋮ On extensibility of proof checkers ⋮ Formalization of a λ-calculus with explicit substitutions in Coq ⋮ Checking algorithms for Pure Type Systems ⋮ Closure under alpha-conversion ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Typed operational semantics for higher-order subtyping. ⋮ An extensible equality checking algorithm for dependent type theories ⋮ The locally nameless representation ⋮ An algorithm for checking incomplete proof objects in type theory with localization and unification ⋮ Proof Pearl: Abella Formalization of λ-Calculus Cube Property ⋮ Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms ⋮ External and internal syntax of the \(\lambda \)-calculus ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle ⋮ Foundations for extensible objects with roles ⋮ Mechanizing metatheory without typing contexts

This page was built for publication: