Pre-logical Relations

Furio Honsell, Donald Sannella

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We study a weakening of the notion of logical relations, called pre-logical relations, that has many of the features that make logical relations so useful as well as further algebraic properties including composability. The basic idea is simply to require the reverse implication in the definition of logical relations to hold only for pairs of functions that are expressible by the same lambda term. Pre-logical relations are the minimal weakening of logical relations that gives composability for extensional structures and simultaneously the most liberal definition that gives the Basic Lemma. The use of pre-logical relations in place of logical relations gives an improved version of Mitchell’s representation independence theorem which characterizes observational equivalence for all signatures rather than just for first-order signatures. Pre-logical relations can be used in place of logical relations to give an account of data refi-nement where the fact that pre-logical relations compose explains why stepwise refinement is sound.
Original languageEnglish
Title of host publicationComputer Science Logic
Subtitle of host publication13th International Workshop, CSL’99 8th Annual Conference of the EACSL Madrid, Spain, September 20–25, 1999 Proceedings
EditorsJörg Flum, Mario Rodriguez-Artalejo
PublisherSpringer
Pages546-561
Number of pages16
ISBN (Electronic)978-3-540-48168-3
ISBN (Print)978-3-540-66536-6
DOIs
Publication statusPublished - 1999

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
Volume1683
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'Pre-logical Relations'. Together they form a unique fingerprint.

Cite this