Automath
From MaRDI portal
Cited in
(only showing first 100 items - show all)- 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
- A proof description language and its reduction system
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
- On the syntax of Martin-Löf's type theories
- The calculus of constructions
- On Church's formal theory of functions and functionals. The - calculus: Connections to higher type recursion theory, proof theory, category theory
- CPS translations and applications: The cube and beyond
- Higher-order rewrite systems and their confluence
- A notation for lambda terms. A generalization of environments
- What does logic have to tell us about mathematical proofs?
- The logical study of science
- Logic, methodology and philosophy of science, VI. Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science, Hannover, 1979
- Between constructive mathematics and PROLOG
- Type checking with universes
- Program development in constructive type theory
- On the adequacy of representing higher order intuitionistic logic as a pure type system
- Comprehension categories and the semantics of type dependency
- 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
- From constructivism to computer science
- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
- Order-sorted inductive types
- Perpetual reductions in -calculus
- A syntactic proof of the conservativity of \(\lambda_\omega\) over \(\lambda_2\)
- Coq
- Typability and type checking in System F are equivalent and undecidable
- On -conversion in the -cube and the combination with abbreviations
- Ordinals and ordinal functions representable in the simply typed lambda calculus
- Combinatory reduction systems: Introduction and survey
- ILTP
- Isabelle
- Structured theory presentations and logic representations
- \(F\)-semantics for type assignment systems
- PyRes
- Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
- Algebraic domains of natural transformations
- A unified approach to type theory through a refined -calculus
- Strong normalization for non-structural subtyping via saturated sets
- 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
- Comparing cubes of typed and type assignment systems
- A useful -notation
- SUBSEXPL
- Theorema
- On the semantics of the universal quantifier
- The expansion postponement in pure type systems
- Termination of system F-bounded: A complete proof
- Abstract data type systems
- Developing developments
- Typed generic traversal with term rewriting strategies
- Revisiting the notion of function
- ML
- Typing correspondence assertions for communication protocols
- A linear logical framework
- Typed operational semantics for higher-order subtyping.
- Strong normalization from weak normalization by translation into the lambda-I-calculus
- TinkerType
- THINKER
- ASSET
- TAMPR
- On the intuitionistic force of classical search
- Proof-search in type-theoretic languages: An introduction
- On principal types of combinators
- Program development schemata as derived rules
- CCSL
- OMRS
- APTS
- MAYA
- NUML
- Autarkic computations in formal proofs
- The Church-Rosser theorem and quantitative analysis of witnesses
- The role of the Mizar mathematical library for interactive proof development in Mizar
- MetaPRL
- On the number of types
- Isabelle/ZF
- Miranda
- Fibrational modal type theory
- TeXmacs
- A type system for counting instances of software components
- De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case
- De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case
- Lambda-calculus with director strings
- Comparing and implementing calculi of explicit substitutions with eta-reduction
- Relating categorical semantics for intuitionistic linear logic
- Combinatorial topology and constructive mathematics
- Analogical program derivation based on type theory
- Inherited extension of many-sorted theories
- Typing and computational properties of lambda expressions
- The foundation of a generic theorem prover
- Towards a computation system based on set theory
- Matita
- ETPS
- OCaml
- Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus
- Higher order unification via explicit substitutions
This page was built for software: Automath
