Pure type systems with explicit substitutions (Q5371956): Difference between revisions

@@ Property / describes a project that uses @@
+Matita
@@ Property / describes a project that uses: Matita / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Automath
@@ Property / describes a project that uses: Automath / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Towards Normalization by Evaluation for the βη-Calculus of Constructions
+Normal rank
@@ Property / cites work @@
+Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
+Normal rank
@@ Property / cites work @@
+A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance
+Normal rank
@@ Property / cites work @@
+Pure type systems with judgemental equality
@@ Property / cites work: Pure type systems with judgemental equality / rank @@
+Normal rank
@@ Property / cites work @@
+Big-step normalisation
@@ Property / cites work: Big-step normalisation / rank @@
+Normal rank
@@ Property / cites work @@
+The Matita Interactive Theorem Prover
@@ Property / cites work: The Matita Interactive Theorem Prover / rank @@
+Normal rank
@@ Property / cites work @@
+Q4246942
@@ Property / cites work: Q4246942 / rank @@
+Normal rank
@@ Property / cites work @@
+Remarks on the equational theory of non-normalizing pure type systems
+Normal rank
@@ Property / cites work @@
+Domain-free pure type systems
@@ Property / cites work: Domain-free pure type systems / rank @@
+Normal rank
@@ Property / cites work @@
+Pure type systems with explicit substitution
@@ Property / cites work: Pure type systems with explicit substitution / rank @@
+Normal rank
@@ Property / cites work @@
+Confluence properties of weak and strong calculi of explicit substitutions
+Normal rank
@@ Property / cites work @@
+Strong normalization of substitutions
@@ Property / cites work: Strong normalization of substitutions / rank @@
+Normal rank
@@ Property / cites work @@
+A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
+Normal rank
@@ Property / cites work @@
+Internal type theory
@@ Property / cites work: Internal type theory / rank @@
+Normal rank
@@ Property / cites work @@
+A general formulation of simultaneous inductive-recursive definitions in type theory
+Normal rank
@@ Property / cites work @@
+A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation
+Normal rank
@@ Property / cites work @@
+Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
+Normal rank
@@ Property / cites work @@
+Confluence of extensional and non-extensional \(\lambda\)-calculi with explicit substitutions
+Normal rank
@@ Property / cites work @@
+Q4296744
@@ Property / cites work: Q4296744 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4435473
@@ Property / cites work: Q4435473 / rank @@
+Normal rank
@@ Property / cites work @@
+Dependent types and explicit substitutions: a meta-theoretical development
+Normal rank
@@ Property / cites work @@
+Pure Type System conversion is always typable
@@ Property / cites work: Pure Type System conversion is always typable / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1017/s0956796815000210
+Normal rank
@@ Property / OpenAlex ID @@
+W2284245339
@@ Property / OpenAlex ID: W2284245339 / rank @@
+Normal rank