scientific article; zbMATH DE number 512787

MaRDI QIDQ4281480zbMATH OpenFDO

Authors James McKinna, Robert Pollack

Publication date 1993

zbMATH Keywords

generalized type systemspure type systems

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Recommendations

• Some lambda calculus and type theory formalized
• Automath and Pure Type Systems
• Pure type systems with explicit substitutions
• Pure type systems with more liberal rules

Cited in

(35)

• 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
• Pure type systems with explicit substitution
• Specifying type systems
• Pure Type Systems with de Bruijn Indices
• More Church-Rosser proofs (in Isabelle/HOL)
• An algorithm for checking incomplete proof objects in type theory with localization and unification
• scientific article; zbMATH DE number 2154395 (Why is no real title available?)
• Domain-free pure type systems
• Proof pearl: Abella formalization of \(\lambda \)-calculus cube property
• Automath and Pure Type Systems
• An extensible equality checking algorithm for dependent type theories
• Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle
• scientific article; zbMATH DE number 960927 (Why is no real title available?)
• Perspectives of System Informatics
• 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
• Formal verification of algorithm \(\mathcal{W}\): the monomorphic case
• Abstractions for multi-sorted substitutions
• More Church-Rosser proofs in \textsc{Beluga}
• Pure type systems without explicit contexts
• Invertibility in Sequent Calculi
• Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
• External and internal syntax of the \(\lambda \)-calculus

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4281480)