Extensional Rewriting with Sums

DOI10.1007/978-3-540-73228-0_19MaRDI QIDQ3612636zbMATH OpenOpenAlexFDO

Authors Sam Lindley

Publication date 10 March 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73228-0_19

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40)

Recommendations

• A confluent reduction for the extensional typed -calculus with pairs, sums, recursion and terminal object
• scientific article; zbMATH DE number 2185660
• Simulating expansions without expansions
• Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
• Multi-focusing on extensional rewriting with sums

Cited in

(21)

• Rewriting with extensional polymorphic \(\lambda \)-calculus
• The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
• A refined interpretation of intuitionistic logic by means of atomic polymorphism
• The exp-log normal form of types: decomposing extensional equality and representing terms compactly
• A confluent reduction for the extensional typed -calculus with pairs, sums, recursion and terminal object
• Polarised intermediate representation of lambda calculus with sums
• scientific article; zbMATH DE number 2185660 (Why is no real title available?)
• The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
• What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics
• How to prove decidability of equational theories with second-order computation analyser SOL
• Isomorphisms of simple inductive types through extensional rewriting
• Big-step normalisation
• Call-by-name extensionality and confluence
• Simulating expansions without expansions
• Normalization by evaluation for modal dependent type theory
• Multi-focusing on extensional rewriting with sums
• Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
• A new conjecture about identity of proofs
• Deciding equivalence with sums and the empty type
• The naturality of natural deduction
• A local graph-rewriting system for deciding equality in sum-product theories

This page was built for publication: Extensional Rewriting with Sums

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