Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

We propose a calculus of explicit substitutions with de Bruijn indices for implementing objects and functions which is confluent and preserves strong normalization. We start from Abadi and Cardelli’s ς-calculus [1] for the object calculus and from the λυ-calculus [20] for the functional calculus. The de Bruijn setting poses problems when encoding the λυ-calculus within the ς-calculus following the style proposed in [1]. We introduce fields as a primitive construct in the target calculus in order to deal with these difficulties. The solution obtained greatly simplifies the one proposed in [17] in a named variable setting. We also eliminate the conditional rules present in the latter calculus obtaining in this way a full non-conditional first order system.

Original languageEnglish
Title of host publicationComputer Science Logic - 13th International Workshop, CSL 1999 - 8th Annual Conference of the EACSL, Proceedings
EditorsJörg Flum, Mario Rodriguez-Artalejo
Pages204-219
Number of pages16
DOIs
StatePublished - 1999
Event13th International Workshop on Computer Science Logic, CSL 1999 and held as International Workshops on Computer Science Logic, EACSL 1999 - Madrid, Spain
Duration: 20 Sep 199925 Sep 1999

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1683
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference13th International Workshop on Computer Science Logic, CSL 1999 and held as International Workshops on Computer Science Logic, EACSL 1999
Country/TerritorySpain
CityMadrid
Period20/09/9925/09/99

Fingerprint

Dive into the research topics of 'Using fields and explicit substitutions to implement objects and functions in a de Bruijn setting'. Together they form a unique fingerprint.

Cite this