Towards a proof theory of rewriting: The simply typed 2-calculus

DOI10.1016/S0304-3975(96)80713-4MaRDI QIDQ672060zbMATH OpenOpenAlexFDO

Authors Barnaby P. Hilken

Publication date 27 February 1997

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0304-3975(96)80713-4

zbMATH Keywords

catagorical rewritingconfluenceequational theorysimply typed 2\(\lambda\)-calculusword problem

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• The simply typed rewriting calculus
• Proof systems for retracts in simply typed lambda calculus
• scientific article; zbMATH DE number 431764
• scientific article; zbMATH DE number 722285
• A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
• A quantitative model for simply typed λ-calculus
• A unified approach to type theory through a refined -calculus
• Theorem proving for untyped constructive -calculus: Implementation and application
• Denotational semantics of the simplified lambda-mu calculus and a new deduction system of classical type theory
• A completeness result for the simply typed \(\lambda \mu \)-calculus

Cites work

• A confluent reduction for the extensional typed -calculus with pairs, sums, recursion and terminal object
• Combining first order algebraic rewriting systems, recursion and extensional lambda calculi
• Formal category theory: Adjointness for 2-categories
• scientific article; zbMATH DE number 3875232 (Why is no real title available?)
• scientific article; zbMATH DE number 4085643 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 512797 (Why is no real title available?)
• scientific article; zbMATH DE number 3297895 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Simulating expansions without expansions
• The calculus of constructions
• The virtues of eta-expansion

Cited in

(15)

• A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
• Relative full completeness for bicategorical Cartesian closed structure
• scientific article; zbMATH DE number 722285 (Why is no real title available?)
• Axiomatic rewriting theory II: the   -calculus enjoys finite normalisation cones
• scientific article; zbMATH DE number 814613 (Why is no real title available?)
• A rewriting view of simple typing
• Dynamic game semantics
• Coherence for bicategorical cartesian closed structure
• An abstract formulation for rewrite systems
• Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
• Multi-focusing on extensional rewriting with sums
• Proof systems for retracts in simply typed lambda calculus
• A partial metric semantics of higher-order types and approximate program transformations
• Effectful semantics in 2-dimensional categories: premonoidal and Freyd bicategories
• Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonads

This page was built for publication: Towards a proof theory of rewriting: The simply typed \(2\lambda\)-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q672060)