Automath
From MaRDI portal
Software:19182
swMATH7127MaRDI QIDQ19182FDOQ19182
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- 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
- Theoretical Aspects of Computing – ICTAC 2005
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- Title not available (Why is that?)
- Monotone (co)inductive types and positive fixed-point types
- Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach
- Syntactic analysis of \(\eta\)-expansions in pure type systems.
- On preserving the computational content of mathematical proofs: toy examples for a formalising strategy
- Taxonomies of geometric problems
- Fibrational modal type theory
- A proposal for broad spectrum proof certificates
- Variants of the basic calculus of constructions
- The Church-Rosser theorem and quantitative analysis of witnesses
- NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
- Sub-\(\lambda\)-calculi, classified
- Size-based termination of higher-order rewriting
- POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE
- A type system for counting instances of software components
- A modular type-checking algorithm for type theory with singleton types and proof irrelevance
- Intersection types for the resource control lambda calculi
- Title not available (Why is that?)
- A modern elaboration of the ramified theory of types
- Term-space semantics of typed lambda calculus
- Union of Reducibility Candidates for Orthogonal Constructor Rewriting
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Combinatorial topology and constructive mathematics
- Ranking/Unranking of Lambda Terms with Compressed de Bruijn Indices
- Type theory and formalisation of mathematics
- Title not available (Why is that?)
- Analogical program derivation based on type theory
- A note on algebraic semantics for \(\mathsf {S5}\) with propositional quantifiers
- Formalizing Ordinal Partition Relations Using Isabelle/HOL
- Call-by-Name and Call-by-Value in Normal Modal Logic
- Practical Proof Search for Coq by Type Inhabitation
- Title not available (Why is that?)
- Exploring the structure of an algebra text with locales
- Weak normalization implies strong normalization in a class of non-dependent pure type systems
- A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
- Towards a formal framework for heterogeneous relation algebra
- A modular construction of type theories
- Title not available (Why is that?)
- Title not available (Why is that?)
- An introduction to univalent foundations for mathematicians
- Modular properties of algebraic type systems
- On principal types of combinators
- Program development schemata as derived rules
- Linearization of the lambda-calculus and its relation with intersection type systems
- Proof-irrelevance out of excluded-middle and choice in the calculus of constructions
- A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
- On explicit substitutions and names (extended abstract)
- Simplified Reducibility Proofs of Church-Rosser for β- and βη-reduction
- 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
- KI 2004: Advances in Artificial Intelligence
- The variable containment problem
- Integration in Real PCF
- A framework for defining logical frameworks
- 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?)
- 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
- Hyperformulae, Parallel Deductions and Intersection Types
- Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions
- Intersection types for explicit substitutions
- The Girard-Reynolds isomorphism
This page was built for software: Automath
