The following pages link to Automath (Q19182):
Displaying 50 items.
- COMPLETENESS OF SECOND-ORDER PROPOSITIONAL S4 AND H IN TOPOLOGICAL SEMANTICS (Q4961741) (← links)
- THE CONCEPT<i>HORSE</i>IS A CONCEPT (Q4961743) (← links)
- Deriving Efficient Sequential and Parallel Generators for Closed Simply-Typed Lambda Terms and Normal Forms (Q4988930) (← links)
- NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF (Q5001547) (← links)
- (Q5014449) (← links)
- A Formalization of Properties of Continuous Functions on Closed Intervals (Q5041063) (← links)
- Practical Proof Search for Coq by Type Inhabitation (Q5048991) (← links)
- Open problems in rewriting (Q5055780) (← links)
- A termination ordering for higher order rewrite systems (Q5055816) (← links)
- Towards a domain theory for termination proofs (Q5055834) (← links)
- Problems in rewriting III (Q5055847) (← links)
- A recursive path ordering for higher-order terms in η-long β-normal form (Q5055855) (← links)
- Combinatory reduction systems with explicit substitution that preserve strong normalisation (Q5055859) (← links)
- Typed Relational Conversion (Q5056070) (← links)
- Characteristics of de Bruijn’s early proof checker Automath (Q5089679) (← links)
- Formalizing Ordinal Partition Relations Using Isabelle/HOL (Q5094473) (← links)
- Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL (Q5094474) (← links)
- In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming (Q5108530) (← links)
- Relating system F and \(\lambda 2\): a case study in Coq, Abella and Beluga (Q5111317) (← links)
- (Q5140267) (← links)
- Representing Model Theory in a Type-Theoretical Logical Framework (Q5170290) (← links)
- Simplified Reducibility Proofs of Church-Rosser for β- and βη-reduction (Q5178963) (← links)
- A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi (Q5179010) (← links)
- Formalization of constructivity in Automath (Q5187278) (← links)
- Introduction to Type Theory (Q5191087) (← links)
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic (Q5191100) (← links)
- Verified Representations of Landau's "Grundlagen" in the lambda-delta Family and in the Calculus of Constructions (Q5195263) (← links)
- Formalizing Scientifically Applicable Mathematics in a Definitional Framework (Q5195269) (← links)
- Translating between Language and Logic: What Is Easy and What Is Difficult (Q5200012) (← links)
- Licensing the Mizar Mathematical Library (Q5200114) (← links)
- Parsing and Disambiguation of Symbolic Mathematics in the Naproche System (Q5200117) (← links)
- Reconstructing proofs at the assertion level (Q5210809) (← links)
- A practical implementation of simple consequence relations using inductive definitions (Q5234714) (← links)
- A general proof certification framework for modal logic (Q5236558) (← links)
- The infinitary lambda calculus of the infinite eta Böhm trees (Q5269002) (← links)
- Clocked lambda calculus (Q5269007) (← links)
- $\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads (Q5278085) (← links)
- The challenge of computer mathematics (Q5301849) (← links)
- Mechanizing metatheory in a logical framework (Q5308093) (← links)
- Mathematical Knowledge Management (Q5313054) (← links)
- Mathematical Knowledge Management (Q5313058) (← links)
- Pure type systems with explicit substitutions (Q5371956) (← links)
- Refinement Types as Higher-Order Dependency Pairs (Q5389088) (← links)
- Pure Type Systems in Rewriting Logic: Specifying Typed Higher-Order Languages in a First-Order Logical Framework (Q5390279) (← links)
- Computer Science Logic (Q5394574) (← links)
- Computer Science Logic (Q5394575) (← links)
- Theoretical Aspects of Computing – ICTAC 2005 (Q5395103) (← links)
- A logical framework combining model and proof theory (Q5400853) (← links)
- Discriminating Lambda-Terms Using Clocked Boehm Trees (Q5419488) (← links)
- A Critique of a Formalist-Mechanist Version of the Justification of Arguments in Mathematicians' Proof Practices (Q5426521) (← links)
