Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
type: Item
instance of: scholarly article
title: Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
zbMATH Open document ID: 1146.68028
author: Daniel J. Dougherty
author: Silvia Ghilezan
author: Pierre Lescanne
published in: Theoretical Computer Science
publication date: 2008-06-24T00:00:00Z
Mathematics Subject Classification ID: 68N18
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03F05
zbMATH DE Number: 5292221
zbMATH Keywords: intersection-types
zbMATH Keywords: classical logic
zbMATH Keywords: sequent calculus
describes a project that uses: Forsythe
MaRDI profile type: Publication
full work available at URL: j.tcs.2008.01.022
OpenAlex ID: W1980174718
cites work: A symmetric lambda calculus for classical program extraction
cites work: Intersection and union types: Syntax and semantics
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: A filter lambda model and the completeness of type assignment
cites work: Lambda terms for natural deduction, sequent calculus and cut elimination
cites work: On type inference in the intersection type discipline
cites work: Q4473165
cites work: Hyperformulae, Parallel Deductions and Intersection Types
cites work: A new type assignment for λ-terms
cites work: An extension of basic functionality theory for \(\lambda\)-calculus
cites work: Symmetry and Interactivity in Programming
cites work: Normalization without reducibility
cites work: Typed Lambda Calculi and Applications
cites work: Why the usual candidates of reducibility do not work for the symmetric \(\lambda\mu\)-calculus
cites work: The ``relevance'' of intersection and union types
cites work: Intersection and union types in the \(\bar{\lambda}\mu\tilde{\mu}\)-calculus
cites work: Strong Normalization of the Dual Classical Sequent Calculus
cites work: Q4417863
cites work: Tridirectional typechecking
cites work: Coppo-Dezani types do not correspond to propositional logic
cites work: Call-by-value, call-by-name, and strong normalization for the classical sequent calculus
cites work: From polyvariant flow information to intersection and union types
cites work: Q4255509
cites work: Foundations of Software Science and Computation Structures
cites work: Normalization as a homomorphic image of cut-elimination
cites work: Q4783322
cites work: Q4163188
cites work: A lattice-theoretical fixpoint theorem and its applications
cites work: Q4263882
cites work: Principal Type Schemes for the Strict Type Assignment System
cites work: Call-by-value is dual to call-by-name
cites work: Term Rewriting and Applications
cites work: A calculus with polymorphic and polyvariant flow types
cites work: Q4738350
DOI: 10.1016/J.TCS.2008.01.022
description: scientific article; zbMATH DE number 5292221