Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications

DOI10.1016/j.jlamp.2022.100830OpenAlexW4308488466MaRDI QIDQ2683029

Luís Pinto, Maria João. Frade, José Espírito Santo

Publication date: 3 February 2023

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2022.100830

zbMATH Keywords

sequent calculusnatural deductionpermutative conversioncommutative conversionnormal and natural proofsvector notation

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Permutability of proofs in intuitionistic sequent calculi
• Termination of permutative conversions in intuitionistic Gentzen calculi
• Natural deduction with general elimination rules
• A calculus of multiary sequent terms
• Structural Proof Theory as Rewriting
• The correspondence between cut-elimination and normalization
• Types for Proofs and Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications