The following pages link to Automath (Q19182):
Displaying 50 items.
- Abstract data type systems (Q1391729) (← links)
- Developing developments (Q1392147) (← links)
- Typed generic traversal with term rewriting strategies (Q1394988) (← links)
- Revisiting the notion of function (Q1394989) (← links)
- Typing correspondence assertions for communication protocols (Q1399972) (← links)
- A linear logical framework (Q1400718) (← links)
- Typed operational semantics for higher-order subtyping. (Q1401950) (← links)
- Strong normalization from weak normalization by translation into the lambda-I-calculus (Q1426886) (← links)
- On the intuitionistic force of classical search (Q1575923) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- On principal types of combinators (Q1583260) (← links)
- Program development schemata as derived rules (Q1583853) (← links)
- Autarkic computations in formal proofs (Q1610674) (← links)
- The Church-Rosser theorem and quantitative analysis of witnesses (Q1627965) (← links)
- The role of the Mizar mathematical library for interactive proof development in Mizar (Q1663215) (← links)
- On the number of types (Q1708962) (← links)
- Fibrational modal type theory (Q1744413) (← links)
- A type system for counting instances of software components (Q1758151) (← links)
- De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case (Q1763159) (← links)
- De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case (Q1764799) (← links)
- Lambda-calculus with director strings (Q1778107) (← links)
- Comparing and implementing calculi of explicit substitutions with eta-reduction (Q1779307) (← links)
- Relating categorical semantics for intuitionistic linear logic (Q1781095) (← links)
- Combinatorial topology and constructive mathematics (Q1788338) (← links)
- Analogical program derivation based on type theory (Q1802072) (← links)
- Inherited extension of many-sorted theories (Q1816347) (← links)
- Typing and computational properties of lambda expressions (Q1819575) (← links)
- The foundation of a generic theorem prover (Q1823013) (← links)
- Towards a computation system based on set theory (Q1825191) (← links)
- Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus (Q1853595) (← links)
- Higher order unification via explicit substitutions (Q1854337) (← links)
- Descendants and origins in term rewriting. (Q1854348) (← links)
- Integration in Real PCF (Q1854356) (← links)
- Higher-order substitutions (Q1854398) (← links)
- Perpetuality and uniform normalization in orthogonal rewrite systems (Q1854401) (← links)
- Dependent types with subtyping and late-bound overloading (Q1854436) (← links)
- Conservation and uniform normalization in lambda calculi with erasing reductions (Q1854562) (← links)
- A compendium of continuous lattices in MIZAR (Q1868506) (← links)
- Syntactic analysis of \(\eta\)-expansions in pure type systems. (Q1873755) (← links)
- A refinement of de Bruijn's formal language of mathematics (Q1876109) (← links)
- The differential lambda-calculus (Q1884894) (← links)
- Variants of the basic calculus of constructions (Q1885480) (← links)
- Intersection types for explicit substitutions (Q1887145) (← links)
- The Girard-Reynolds isomorphism (Q1887154) (← links)
- Strong normalization in type systems: A model theoretical approach (Q1891251) (← links)
- A formal semantics for DAI language NUML (Q1894325) (← links)
- On completeness and cocompleteness in and around small categories (Q1896485) (← links)
- Understanding uniformity in Feferman's explicit mathematics (Q1899146) (← links)
- Strong normalization and typability with intersection types (Q1924327) (← links)
- N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker (Q1935352) (← links)
