Essential and relational models

Intersection type assignment systems can be used as a general framework for building logical models of λ-calculus that allow to reason about the denotation of terms in a finitary way. We define essential models (a new class of logical models) through a parametric type assignment system using non-ide...

Full description

Saved in:
Bibliographic Details
Published in:Mathematical structures in computer science 2017-06, Vol.27 (5), p.626-650
Main Authors: PAOLINI, LUCA, PICCOLO, MAURO, RONCHI DELLA ROCCA, SIMONA
Format: Article
Language:English
Subjects:
Buildings
Categories
Computer simulation
Intersections
Mathematical models
Parameters
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Intersection type assignment systems can be used as a general framework for building logical models of λ-calculus that allow to reason about the denotation of terms in a finitary way. We define essential models (a new class of logical models) through a parametric type assignment system using non-idempotent intersection types. Under an interpretation of terms based on typings instead than the usual one based on types, every suitable instance of the parameters induces a λ-model, whose theory is sensible. We prove that this type assignment system provides a logical description of a family of λ-models arising from a category of sets and relations.
ISSN:0960-1295
1469-8072
DOI:10.1017/S0960129515000316