The following pages link to Automath (Q19182):
Displaying 50 items.
- Reducibility: a ubiquitous method in lambda calculus with intersection types (Q2842839) (← links)
- MathLang: experience-driven development of a new mathematical language (Q2847398) (← links)
- Rewriting calculus with(out) types (Q2851046) (← links)
- A framework for defining logical frameworks (Q2864157) (← links)
- Computerizing mathematical text with MathLang (Q2866734) (← links)
- Reduction and conversion strategies for the calculus of (co)inductive constructions. I (Q2866803) (← links)
- \textsc{Plat}{\(\Omega\)}: a mediator between text-editors and proof assistance systems (Q2867939) (← links)
- Sub-\(\lambda\)-calculi, classified (Q2870319) (← links)
- A logical framework with explicit conversions (Q2871837) (← links)
- Encoding functional relations in Scunak (Q2871865) (← links)
- Inductive and coinductive components of corecursive functions in Coq (Q2873661) (← links)
- In memoriam: Nicolaas Govert de Bruijn (1918--2012). Mathematics and language: the Automath project (Q2878128) (← links)
- A System F accounting for scalars (Q2881078) (← links)
- A bi-directional refinement algorithm for the calculus of (co)inductive constructions (Q2881085) (← links)
- Preservation of strong normalisation modulo permutations for the structural \(\lambda\)-calculus (Q2881096) (← links)
- A Proof Theoretic Interpretation of Model Theoretic Hiding (Q2890327) (← links)
- The Complexity of Inhabitation with Explicit Intersection (Q2897957) (← links)
- The Inverse Lambda Calculus Algorithm for Typed First Order Logic Lambda Calculus and Its Application to Translating English to FOL (Q2900507) (← links)
- Book review of: H. Barendregt et al., Lambda calculus with types (Q2922875) (← links)
- Proof Assistants for Natural Language Semantics (Q2963996) (← links)
- A Monotonic Higher-Order Semantic Path Ordering (Q2996192) (← links)
- Realizability and Parametricity in Pure Type Systems (Q3000602) (← links)
- A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems (Q3003307) (← links)
- A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance (Q3003322) (← links)
- (Q3024854) (← links)
- (Q3026376) (← links)
- (Q3030827) (← links)
- (Q3075241) (← links)
- A Cut-Free Sequent Calculus for Pure Type Systems Verifying the Structural Rules of Gentzen/Kleene (Q3079922) (← links)
- Equivalence-Checking with Infinite-State Systems: Techniques and Results (Q3085977) (← links)
- (Q3086726) (← links)
- A Proposal for Broad Spectrum Proof Certificates (Q3100201) (← links)
- Intersection Types for the Resource Control Lambda Calculi (Q3105748) (← links)
- CPO-models for second order lambda calculus with recursive types and subtyping (Q3142273) (← links)
- Monadic encapsulation of effects: a revised approach (extended version) (Q3150208) (← links)
- Unified Syntax with Iso-types (Q3179296) (← links)
- Automath Type Inclusion in Barendregt’s Cube (Q3194722) (← links)
- The computability path ordering (Q3196359) (← links)
- (Q3210191) (← links)
- Kripke Semantics for Martin-L\"of's Extensional Type Theory (Q3224684) (← links)
- A Type Theory for Probabilistic $$\lambda $$–calculus (Q3297838) (← links)
- (Q3300787) (← links)
- (Q3300788) (← links)
- Intuitionistic categorial grammar (Q3348895) (← links)
- Remarks on the equational theory of non-normalizing pure type systems (Q3377459) (← links)
- Pure type systems with judgemental equality (Q3377462) (← links)
- (Q3431410) (← links)
- Constructive analysis, types and exact real numbers (Q3431542) (← links)
- Ranking/Unranking of Lambda Terms with Compressed de Bruijn Indices (Q3453110) (← links)
- Call-by-Name and Call-by-Value in Normal Modal Logic (Q3498449) (← links)
