Automath
From MaRDI portal
Software:19182
No author found.
Related Items (only showing first 100 items - show all)
Structured theory presentations and logic representations ⋮ \(F\)-semantics for type assignment systems ⋮ Canonicity of weak \(\omega\)-groupoid laws using parametricity theory ⋮ Selected papers on AUTOMATH, dedicated to N. G. de Bruijn ⋮ Coq formalization of the higher-order recursive path ordering ⋮ Algebraic domains of natural transformations ⋮ A unified approach to type theory through a refined \(\lambda\)-calculus ⋮ Strong normalization for non-structural subtyping via saturated sets ⋮ On the syntax of Martin-Löf's type theories ⋮ Embedding complex decision procedures inside an interactive theorem prover. ⋮ Formalizing process algebraic verifications in the calculus of constructions ⋮ Strong normalization from weak normalization in typed \(\lambda\)-calculi ⋮ Bridging Curry and Church's typing style ⋮ The calculus of constructions ⋮ Choices in representation and reduction strategies for lambda terms in intensional contexts ⋮ Comparing cubes of typed and type assignment systems ⋮ A useful \(\lambda\)-notation ⋮ Innovations in computational type theory using Nuprl ⋮ SAD as a mathematical assistant -- how should we go from here to there? ⋮ Supporting the formal verification of mathematical texts ⋮ Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics ⋮ On the semantics of the universal quantifier ⋮ The decidability of a fragment of \(\text{BB}'\text{IW}\)-logic ⋮ Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants ⋮ Formal and efficient primality proofs by use of computer algebra oracles ⋮ The expansion postponement in pure type systems ⋮ A decidable theory of type assignment ⋮ Higher-order subtyping and its decidability ⋮ Strong normalisation in the \(\pi\)-calculus ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ Light affine lambda calculus and polynomial time strong normalization ⋮ CPS translations and applications: The cube and beyond ⋮ The Girard-Reynolds isomorphism (second edition) ⋮ Termination of system \(F\)-bounded: A complete proof ⋮ Higher-order rewrite systems and their confluence ⋮ Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types ⋮ Internal diagrams and archetypal reasoning in category theory ⋮ A notation for lambda terms. A generalization of environments ⋮ Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters ⋮ A scalable module system ⋮ Intuitionistic completeness of first-order logic ⋮ What does logic have to tell us about mathematical proofs? ⋮ Monad transformers as monoid transformers ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Coalgebras in functional programming and type theory ⋮ Do-it-yourself type theory ⋮ Constructive system for automatic program synthesis ⋮ The logical study of science ⋮ How to assign ordinal numbers to combinatory terms with polymorphic types ⋮ Logic, methodology and philosophy of science, VI. Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science, Hannover, 1979 ⋮ A prismoid framework for languages with resources ⋮ Representing model theory in a type-theoretical logical framework ⋮ Applications of real number theorem proving in PVS ⋮ Between constructive mathematics and PROLOG ⋮ On strong normalization and type inference in the intersection type discipline ⋮ Type checking with universes ⋮ Uniformity and the Taylor expansion of ordinary lambda-terms ⋮ Program development in constructive type theory ⋮ On the adequacy of representing higher order intuitionistic logic as a pure type system ⋮ Comparing Hagino's categorical programming language and typed lambda- calculi ⋮ Computational interpretations of linear logic ⋮ Using typed lambda calculus to implement formal systems on a machine ⋮ Definition and basic properties of the Deva meta-calculus ⋮ The vectorial \(\lambda\)-calculus ⋮ Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms ⋮ Preface to the special volume ⋮ Comprehension categories and the semantics of type dependency ⋮ Thirty-five years of automating mathematics. Dedicated to 35 years of de Bruijn's Automath ⋮ The correctness of Newman's typability algorithm and some of its extensions ⋮ Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. ⋮ Typing termination in a higher-order concurrent imperative language ⋮ Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician ⋮ N. G. de Bruijn's contribution to the formalization of mathematics ⋮ Isomorphism is equality ⋮ The semantics of second-order lambda calculus ⋮ Inference rules using local contexts ⋮ Verifying programs in the calculus of inductive constructions ⋮ Type inference for pure type systems ⋮ A note on complexity measures for inductive classes in constructive type theory ⋮ Telescopic mappings in typed lambda calculus ⋮ From constructivism to computer science ⋮ Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering ⋮ Analysis of a clock synchronization protocol for wireless sensor networks ⋮ Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions ⋮ Order-sorted inductive types ⋮ Perpetual reductions in \(\lambda\)-calculus ⋮ A syntactic proof of the conservativity of \(\lambda_\omega\) over \(\lambda_2\) ⋮ Proof assistants: history, ideas and future ⋮ A compact kernel for the calculus of inductive constructions ⋮ Justification of the structural synthesis of programs ⋮ Programs as proofs: A synopsis ⋮ Realizability and intuitionistic logic ⋮ Typability and type checking in System F are equivalent and undecidable ⋮ On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations ⋮ Ordinals and ordinal functions representable in the simply typed lambda calculus ⋮ A proof description language and its reduction system ⋮ Propositions and specifications of programs in Martin-Löf's type theory ⋮ Combinatory reduction systems: Introduction and survey ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction ⋮ Syntactic control of concurrency
This page was built for software: Automath
