The following pages link to Automath (Q19182):
Displaying 36 items.
- KI 2004: Advances in Artificial Intelligence (Q5450782) (← links)
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System (Q5452598) (← links)
- Erasure and Polymorphism in Pure Type Systems (Q5458371) (← links)
- Artificial Intelligence and Symbolic Computation (Q5464706) (← links)
- Frontiers of Combining Systems (Q5491909) (← links)
- On Correctness of Mathematical Texts from a Logical and Practical Point of View (Q5505538) (← links)
- (Q5610115) (← links)
- (Q5667469) (← links)
- A Complete Mechanization of Second-Order Type Theory (Q5667481) (← links)
- Proof-irrelevance out of excluded-middle and choice in the calculus of constructions (Q5687912) (← links)
- Linearization of the lambda-calculus and its relation with intersection type systems (Q5692152) (← links)
- Modelling general recursion in type theory (Q5697711) (← links)
- (Q5714439) (← links)
- On the Stability by Union of Reducibility Candidates (Q5758042) (← links)
- (Q5875422) (← links)
- The practice of logical frameworks (Q5878905) (← links)
- A rewriting coherence theorem with applications in homotopy type theory (Q5879270) (← links)
- Typed equivalence, type assignment, and type containment (Q5881295) (← links)
- A modular construction of type theories (Q5883738) (← links)
- Inductively defined types in the Calculus of Constructions (Q5887516) (← links)
- Topological models for higher order control flow (Q5890044) (← links)
- Least and Greatest Fixed Points in Linear Logic (Q5892168) (← links)
- Types for Proofs and Programs (Q5898169) (← links)
- Mathematical Knowledge Management (Q5898522) (← links)
- Consistency and Completeness of Rewriting in the Calculus of Constructions (Q5900438) (← links)
- A correspondence between Martin-Löf type theory, the ramified theory of types and pure type systems (Q5939957) (← links)
- Objects and their lambda calculus (Q5941197) (← links)
- On the role of OpenMath in interactive mathematical documents (Q5950932) (← links)
- MBase: Representing knowledge and context for the integration of mathematical software systems (Q5950933) (← links)
- Studies of a theory of specifications with built-in program extraction (Q5951523) (← links)
- Inductive-data-type systems (Q5958292) (← links)
- Proof by computation in the Coq system (Q5958299) (← links)
- Least and greatest fixed points in intuitionistic natural deduction (Q5958300) (← links)
- Weak normalization implies strong normalization in a class of non-dependent pure type systems (Q5958619) (← links)
- Subtyping dependent types (Q5958760) (← links)
- An induction principle for pure type systems (Q5958776) (← links)
