The following pages link to Automath (Q19182):
Displaying 50 items.
- Canonicity of weak \(\omega\)-groupoid laws using parametricity theory (Q283766) (← links)
- Bridging Curry and Church's typing style (Q334149) (← links)
- A decidable theory of type assignment (Q365669) (← links)
- Internal diagrams and archetypal reasoning in category theory (Q382414) (← links)
- A scalable module system (Q391632) (← links)
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- How to assign ordinal numbers to combinatory terms with polymorphic types (Q453195) (← links)
- Applications of real number theorem proving in PVS (Q469367) (← links)
- The vectorial \(\lambda\)-calculus (Q529049) (← links)
- Preface to the special volume (Q534064) (← links)
- The correctness of Newman's typability algorithm and some of its extensions (Q549191) (← links)
- The decidability of a fragment of \(\text{BB}'\text{IW}\)-logic (Q596035) (← links)
- Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants (Q597106) (← links)
- Formal and efficient primality proofs by use of computer algebra oracles (Q597112) (← links)
- Higher-order subtyping and its decidability (Q598199) (← links)
- Strong normalisation in the \(\pi\)-calculus (Q598201) (← links)
- Monad transformers as monoid transformers (Q615955) (← links)
- Coalgebras in functional programming and type theory (Q639643) (← links)
- A prismoid framework for languages with resources (Q654907) (← links)
- Representing model theory in a type-theoretical logical framework (Q654913) (← links)
- Comparing Hagino's categorical programming language and typed lambda- calculi (Q685425) (← links)
- Computational interpretations of linear logic (Q685430) (← links)
- Using typed lambda calculus to implement formal systems on a machine (Q688571) (← links)
- Definition and basic properties of the Deva meta-calculus (Q688825) (← links)
- Thirty-five years of automating mathematics. Dedicated to 35 years of de Bruijn's Automath (Q701700) (← links)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. (Q703860) (← links)
- Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician (Q740456) (← links)
- N. G. de Bruijn's contribution to the formalization of mathematics (Q740481) (← links)
- Isomorphism is equality (Q740487) (← links)
- The semantics of second-order lambda calculus (Q751294) (← links)
- Inference rules using local contexts (Q751642) (← links)
- Telescopic mappings in typed lambda calculus (Q757027) (← links)
- Analysis of a clock synchronization protocol for wireless sensor networks (Q764293) (← links)
- Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions (Q764331) (← links)
- Realizability and intuitionistic logic (Q792319) (← links)
- Propositions and specifications of programs in Martin-Löf's type theory (Q800719) (← links)
- Syntactic control of concurrency (Q817845) (← links)
- Coq formalization of the higher-order recursive path ordering (Q843949) (← links)
- Choices in representation and reduction strategies for lambda terms in intensional contexts (Q861365) (← links)
- Innovations in computational type theory using Nuprl (Q865639) (← links)
- SAD as a mathematical assistant -- how should we go from here to there? (Q865654) (← links)
- Supporting the formal verification of mathematical texts (Q865656) (← links)
- Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics (Q865658) (← links)
- Light affine lambda calculus and polynomial time strong normalization (Q877259) (← links)
- The Girard-Reynolds isomorphism (second edition) (Q879366) (← links)
- Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types (Q880987) (← links)
- Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters (Q884953) (← links)
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility (Q896904) (← links)
- Do-it-yourself type theory (Q911744) (← links)
- Constructive system for automatic program synthesis (Q912589) (← links)
