Authors: Dougherty, Daniel
Ghilezan, Silvia 
Lescanne, Pierre
Title: Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: Extending the Coppo-Dezani heritage
Journal: Theoretical Computer Science
Volume: 398
Issue: 1-3
First page: 114
Last page: 128
Issue Date: 28-May-2008
Rank: M22
ISSN: 0304-3975
DOI: 10.1016/j.tcs.2008.01.022
Abstract: 
We develop an intersection type system for the over(λ, -) μ over(μ, ̃) calculus of Curien and Herbelin. This calculus provides a symmetric computational interpretation of classical sequent style logic and gives a simple account of call-by-name and call-by-value. The present system improves upon earlier type disciplines for over(λ, -) μ over(μ, ̃): in addition to characterizing the over(λ, -) μ over(μ, ̃) expressions that are strongly normalizing under free (unrestricted) reduction, the system enjoys the Subject Reduction and the Subject Expansion properties.
Keywords: Classical logic | Intersection-types | Sequent calculus
Publisher: Elsevier

Show full item record

SCOPUSTM   
Citations

15
checked on Sep 16, 2022

Page view(s)

16
checked on Oct 1, 2022

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.