The following pages link to Automath (Q19182):
Displaying 50 items.
- On strong normalization and type inference in the intersection type discipline (Q930868) (← links)
- Uniformity and the Taylor expansion of ordinary lambda-terms (Q944386) (← links)
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms (Q964000) (← links)
- Typing termination in a higher-order concurrent imperative language (Q979082) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- A compact kernel for the calculus of inductive constructions (Q1040007) (← links)
- Justification of the structural synthesis of programs (Q1051416) (← links)
- Programs as proofs: A synopsis (Q1051424) (← links)
- A proof description language and its reduction system (Q1055769) (← links)
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction (Q1075050) (← links)
- On the syntax of Martin-Löf's type theories (Q1099173) (← links)
- The calculus of constructions (Q1108266) (← links)
- On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory (Q1120558) (← links)
- CPS translations and applications: The cube and beyond (Q1125574) (← links)
- Higher-order rewrite systems and their confluence (Q1127334) (← links)
- A notation for lambda terms. A generalization of environments (Q1129257) (← links)
- What does logic have to tell us about mathematical proofs? (Q1135835) (← links)
- The logical study of science (Q1164615) (← links)
- Logic, methodology and philosophy of science, VI. Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science, Hannover, 1979 (Q1166495) (← links)
- Between constructive mathematics and PROLOG (Q1173742) (← links)
- Type checking with universes (Q1177937) (← links)
- Program development in constructive type theory (Q1190474) (← links)
- On the adequacy of representing higher order intuitionistic logic as a pure type system (Q1194249) (← links)
- Comprehension categories and the semantics of type dependency (Q1208414) (← links)
- Verifying programs in the calculus of inductive constructions (Q1267035) (← links)
- Type inference for pure type systems (Q1271309) (← links)
- A note on complexity measures for inductive classes in constructive type theory (Q1271558) (← links)
- From constructivism to computer science (Q1274450) (← links)
- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering (Q1275015) (← links)
- Order-sorted inductive types (Q1286367) (← links)
- Perpetual reductions in \(\lambda\)-calculus (Q1286373) (← links)
- A syntactic proof of the conservativity of \(\lambda_\omega\) over \(\lambda_2\) (Q1288430) (← links)
- Typability and type checking in System F are equivalent and undecidable (Q1302292) (← links)
- On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations (Q1302298) (← links)
- Ordinals and ordinal functions representable in the simply typed lambda calculus (Q1302304) (← links)
- Combinatory reduction systems: Introduction and survey (Q1314356) (← links)
- Structured theory presentations and logic representations (Q1326777) (← links)
- \(F\)-semantics for type assignment systems (Q1329739) (← links)
- Selected papers on AUTOMATH, dedicated to N. G. de Bruijn (Q1340050) (← links)
- Algebraic domains of natural transformations (Q1349657) (← links)
- A unified approach to type theory through a refined \(\lambda\)-calculus (Q1349674) (← links)
- Strong normalization for non-structural subtyping via saturated sets (Q1351999) (← links)
- Embedding complex decision procedures inside an interactive theorem prover. (Q1353946) (← links)
- Formalizing process algebraic verifications in the calculus of constructions (Q1355748) (← links)
- Strong normalization from weak normalization in typed \(\lambda\)-calculi (Q1357009) (← links)
- Comparing cubes of typed and type assignment systems (Q1365249) (← links)
- A useful \(\lambda\)-notation (Q1365680) (← links)
- On the semantics of the universal quantifier (Q1371430) (← links)
- The expansion postponement in pure type systems (Q1375333) (← links)
- Termination of system \(F\)-bounded: A complete proof (Q1383151) (← links)
