Publication:4281480
From MaRDI portal
zbMath0835.68068MaRDI QIDQ4281480
Publication date: 1993
68Q45: Formal languages and automata
Related Items
More Church-Rosser proofs (in Isabelle/HOL), An algorithm for checking incomplete proof objects in type theory with localization and unification, Proof Pearl: Abella Formalization of λ-Calculus Cube Property, An extensible equality checking algorithm for dependent type theories, Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle, Finitary type theories with and without contexts, Rensets and renaming-based recursion for syntax with bindings extended version, Higher-order subtyping and its decidability, Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms, External and internal syntax of the \(\lambda \)-calculus, Typed operational semantics for higher-order subtyping., Foundations for extensible objects with roles, The locally nameless representation, \(\mathrm{HO}\pi\) in Coq, Mechanizing metatheory without typing contexts, Types for modules, A canonical locally named representation of binding