Automath
From MaRDI portal
Software:19182
swMATH7127MaRDI QIDQ19182FDOQ19182
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- A general method for proving the normalization theorem for first and second order typed λ-calculi
- Title not available (Why is that?)
- Title not available (Why is that?)
- Revisiting the notion of function
- Equivalences between pure type systems and systems of illative combinatory logic
- Open problems in rewriting
- Towards a domain theory for termination proofs
- A note on complexity measures for inductive classes in constructive type theory
- A general proof certification framework for modal logic
- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
- \(F\)-semantics for type assignment systems
- A syntactic proof of the conservativity of \(\lambda_\omega\) over \(\lambda_2\)
- A rewriting view of simple typing
- A useful \(\lambda\)-notation
- Automated deduction and knowledge management in geometry
- Pure type systems with explicit substitution
- On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations
- Ordinals and ordinal functions representable in the simply typed lambda calculus
- Strong normalization with singleton types
- Typed Relational Conversion
- Building Mathematics-Based Software Systems to Advance Science and Create Knowledge
- Inductively defined types in the Calculus of Constructions
- A proof-theoretic foundation of abortive continuations
- Title not available (Why is that?)
- Between constructive mathematics and PROLOG
- A Review of Mathematical Knowledge Management
- Type checking with universes
- A relevant analysis of natural deduction
- Translating between language and logic: what is easy and what is difficult
- Comparing and implementing calculi of explicit substitutions with eta-reduction
- Comparing calculi of explicit substitutions with eta-reduction
- Program development in constructive type theory
- Algebraic domains of natural transformations
- On the adequacy of representing higher order intuitionistic logic as a pure type system
- Typing Correspondence Assertions for Communication Protocols
- Title not available (Why is that?)
- Formalizing process algebraic verifications in the calculus of constructions
- Title not available (Why is that?)
- Proof-search in type-theoretic languages: An introduction
- Understanding uniformity in Feferman's explicit mathematics
- The expansion postponement in pure type systems
- Title not available (Why is that?)
- A focused sequent calculus framework for proof search in pure type systems
- Studies of a theory of specifications with built-in program extraction
- On principal types of combinators
- A higher-order calculus and theory abstraction
- Completeness of second-order propositional S4 and H in topological semantics
- On the intuitionistic force of classical search (extended abstract)
- 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
- Classical \(F_{\omega}\), orthogonality and symmetric candidates
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- On explicit substitutions and names (extended abstract)
- Inductive-data-type systems
- The computability path ordering
- Strong normalization for non-structural subtyping via saturated sets
- Reduction and conversion strategies for the calculus of (co)inductive constructions. I
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Coq formalization of the higher-order recursive path ordering
- Consistency and Completeness of Rewriting in the Calculus of Constructions
- Strong normalization in type systems: A model theoretical approach
- Least and greatest fixed points in intuitionistic natural deduction
- KI 2004: Advances in Artificial Intelligence
- The variable containment problem
- Integration in Real PCF
- A framework for defining logical frameworks
- In praise of impredicativity: a contribution to the formalization of meta-programming
- Title not available (Why is that?)
- Pure type systems in rewriting logic: specifying typed higher-order languages in a first-order logical framework
- Logic, methodology and philosophy of science, VI. Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science, Hannover, 1979
- MBase: Representing knowledge and context for the integration of mathematical software systems
- Computer Science Logic
- Choices in representation and reduction strategies for lambda terms in intensional contexts
- Supporting the formal verification of mathematical texts
- Strong normalization from weak normalization by translation into the lambda-I-calculus
- Definitions by rewriting in the Calculus of Constructions
- Reductions, intersection types, and explicit substitutions
- Abstract data type systems
- A Complete Mechanization of Second-Order Type Theory
- A notation for lambda terms. A generalization of environments
- Type inference for pure type systems
- Higher order unification via explicit substitutions
- Title not available (Why is that?)
- Simplified reducibility proofs of Church-Rosser for \({\beta}\)- and \({\beta}{\eta}\)-reduction
- Typing correspondence assertions for communication protocols
- The Girard-Reynolds isomorphism (second edition)
- Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types
- Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters
- 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
- On the Stability by Union of Reducibility Candidates
- On the semantics of the universal quantifier
- Strong normalization from weak normalization in typed \(\lambda\)-calculi
- Strong normalisation in two Pure Pattern Type Systems
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
- Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions
This page was built for software: Automath
