Automath - MaRDI portal

Cited in

(only showing first 100 items - show all)

A bi-directional refinement algorithm for the calculus of (co)inductive constructions
Studies of a theory of specifications with built-in program extraction
Intuitionistic completeness of first-order logic
Monad transformers as monoid transformers
The practice of logical frameworks
Linearization of the lambda-calculus and its relation with intersection type systems
Classical $F_{\omega}$, orthogonality and symmetric candidates
Proof-irrelevance out of excluded-middle and choice in the calculus of constructions
Hyperformulae, parallel deductions and intersection types
On the intuitionistic force of classical search (extended abstract)
Completeness of second-order propositional S4 and H in topological semantics
A rewriting coherence theorem with applications in homotopy type theory
A recursive path ordering for higher-order terms in η-long β-normal form
Combinatory reduction systems with explicit substitution that preserve strong normalisation
Problems in rewriting III
scientific article; zbMATH DE number 1759491 (Why is no real title available?)
Confluency and strong normalizability of call-by-value $\lambda \mu$-calculus
Dependent types with subtyping and late-bound overloading
Conservation and uniform normalization in lambda calculi with erasing reductions
Perpetuality and uniform normalization in orthogonal rewrite systems
Third-order matching in the polymorphic lambda calculus
A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
Characteristics of de Bruijn’s early proof checker Automath
Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants
A logical framework combining model and proof theory
A short note on type-inhabitation: formula-trees vs. game semantics
Lambda-calculus with director strings
Comparing Hagino's categorical programming language and typed lambda- calculi
Definition and basic properties of the Deva meta-calculus
Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers
Formalizing Scientifically Applicable Mathematics in a Definitional Framework
On explicit substitutions and names (extended abstract)
Dependency Tree Automata
What does logic have to tell us about mathematical proofs?
A general method for proving the normalization theorem for first and second order typed λ-calculi
scientific article; zbMATH DE number 1420783 (Why is no real title available?)
The logical study of science
Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
Constructive analysis, types and exact real numbers
A realizability interpretation of Church's simple theory of types
Theoretical Aspects of Computing – ICTAC 2005
Strong normalization for non-structural subtyping via saturated sets
A scalable module system
The computability path ordering
scientific article; zbMATH DE number 1231611 (Why is no real title available?)
Monotone (co)inductive types and positive fixed-point types
A formalization of properties of continuous functions on closed intervals
Revisiting the notion of function
A flexible framework for visualisation of computational properties of general explicit substitutions calculi
Inductive-data-type systems
Computer Science Logic
scientific article; zbMATH DE number 1156717 (Why is no real title available?)
scientific article; zbMATH DE number 1231697 (Why is no real title available?)
scientific article; zbMATH DE number 2182487 (Why is no real title available?)
Genericity and the $\pi$-calculus
Reduction and conversion strategies for the calculus of (co)inductive constructions. I
Equivalences between pure type systems and systems of illative combinatory logic
Preservation of strong normalisation modulo permutations for the structural $\lambda$-calculus
On the role of OpenMath in interactive mathematical documents
Thirty-five years of automating mathematics. Dedicated to 35 years of de Bruijn's Automath
Do-it-yourself type theory
A practical implementation of simple consequence relations using inductive definitions
Formalizing ordinal partition relations using Isabelle/HOL
A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
Pure type systems with judgemental equality
A unified approach to type theory through a refined -calculus
Justification of the structural synthesis of programs
Open problems in rewriting
Towards a domain theory for termination proofs
A simple proof of second-order strong normalization with permutative conversions
Inherited extension of many-sorted theories
\textsc{Plat}{$\Omega$}: a mediator between text-editors and proof assistance systems
On the intuitionistic force of classical search
scientific article; zbMATH DE number 2090721 (Why is no real title available?)
Syntactic analysis of $\eta$-expansions in pure type systems.
CPS translations and applications: The cube and beyond
The Complexity of Inhabitation with Explicit Intersection
Introduction to Type Theory
Representing model theory in a type-theoretical logical framework
The Impact of the Lambda Calculus in Logic and Computer Science
Verified representations of Landau's ``Grundlagen in the $\lambda\delta$ family and in the calculus of constructions
scientific article; zbMATH DE number 1670760 (Why is no real title available?)
The foundation of a generic theorem prover
On preserving the computational content of mathematical proofs: toy examples for a formalising strategy
\texttt{slepice}: towards a verified implementation of type theory in type theory
scientific article; zbMATH DE number 2003160 (Why is no real title available?)
scientific article; zbMATH DE number 2154392 (Why is no real title available?)
Taxonomies of geometric problems
Coq formalization of the higher-order recursive path ordering
A Type Theory for Probabilistic $$\lambda $$–calculus
Canonicity of weak -groupoid laws using parametricity theory
The correctness of Newman's typability algorithm and some of its extensions
On the number of types
A note on complexity measures for inductive classes in constructive type theory
Strong normalization in type systems: A model theoretical approach
Studying provability in implicational intuitionistic logic: the formula tree approach
MathLang: experience-driven development of a new mathematical language
Propositions and specifications of programs in Martin-Löf's type theory
First order logic with domain conditions
Encoding functional relations in Scunak

This page was built for software: Automath