scientific article; zbMATH DE number 512787
From MaRDI portal
Publication:4281480
zbMath0835.68068MaRDI QIDQ4281480
Publication date: 1993
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
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
