On -conversion in the -cube and the combination with abbreviations

DOI10.1016/S0168-0072(98)00019-0MaRDI QIDQ1302298zbMATH OpenOpenAlexFDO

Authors Fairouz Kamareddine, Roel Bloo, Rob Nederpelt

Publication date 15 February 2000

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0168-0072(98)00019-0

zbMATH Keywords

normalizationtyped \(\lambda\)-calculus\(\lambda\)-cube\(\Pi\)-conversion\(\Pi\)-reductionabbreviationsabstraction operatorssubject-reduction

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 5778093
• Pedagogical lambda-cube: the \(\lambda^{2}\) case
• From λ to π; or, Rediscovering continuations
• Canonical typing and ∏-conversion in the Barendregt Cube
• scientific article; zbMATH DE number 1302024
• The \(\lambda \)-calculus in the \(\pi \)-calculus
• \(\pi\)-calculi
• scientific article; zbMATH DE number 7132707
• Some remarks on \(\pi_\wedge\)
• On confluence in the \(\pi\)-calculus

Cites work

• scientific article; zbMATH DE number 108365 (Why is no real title available?)
• scientific article; zbMATH DE number 1499107 (Why is no real title available?)
• Call-by-name, call-by-value, call-by-need and the linear lambda calculus
• Canonical typing and ∏-conversion in the Barendregt Cube
• Refining reduction in the lambda calculus
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• The Barendregt cube with definitions and generalised reduction
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(10)

• Typed $\lambda$-calculi with one binder
• Automath and Pure Type Systems
• Canonical typing and ∏-conversion in the Barendregt Cube
• Automath type inclusion in Barendregt's cube
• De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case
• An extended type system with lambda-typed lambda-expressions
• Abbreviation templates
• A framework for defining logical frameworks
• Revisiting the notion of function
• scientific article; zbMATH DE number 1302024 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq
• Automath
• LEGO
• TIL

This page was built for publication: On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations

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