Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters

DOI10.1007/S00153-007-0039-1zbMath1117.03020OpenAlexW1989816897MaRDI QIDQ884953

Pierluigi Minari

Publication date: 7 June 2007

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00153-007-0039-1

zbMATH Keywords

lambda calculuselimination of transitivityequational proof systems

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Proof theory in general (including proof-theoretic semantics) (03F03) Combinatory logic and lambda calculus (03B40)

Related Items (2)

Analytic Equational Proof Systems for Combinatory Logic and λ-Calculus:A Survey ⋮ A solution to Curry and Hindley's problem on combinatory strong reduction

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Higher-order subtyping and its decidability
• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Analytic combinatory calculi and the elimination of transitivity
• Some lambda calculus and type theory formalized
• Combinatory logic. Vol. II
• Coercive subtyping for the calculus of constructions
• The Standardization Theorem for λ‐Calculus
• Coherence of subsumption, minimum typing and type-checking in F ≤
• Upper bounds for standardizations and an application
• Coherence and transitivity of subtyping as entailment
• Operational aspects of untyped Normalisation by Evaluation
• Denotational aspects of untyped normalization by evaluation
• Processes, Terms and Cycles: Steps on the Road to Infinity
• Parallel reductions in \(\lambda\)-calculus
• Subtyping dependent types

This page was built for publication: Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters