[TYPES] logical relations

[Don Sannella]

On Thu, 26 Jan 2006 11:13:07 +0000, Uday Reddy wrote:
 > The correspondence between type systems and logics has been known
 > since Curry's time.  Since logical relations are built using that
 > correspondence (times as conjunction, -> as implication and so on.)
 > it was appropriate to call them "logical" relations, i.e., families of
 > relations obtained by treating type constructors as logical connectives.
 >
 > Claudio Hermida tried to squeeze out this correspondence more formally
 > and succeeded to a large degree:
 >
 > @PhDThesis(Hermida-thesis,
 >         Author = "Hermida, C.",
 >         Title = "Fibrations, Logical Predicates and Indeterminantes",
 >         School = "Aarhus University",
 >         Year = "1993"
 >         )

Correction: Edinburgh University.

While I'm here, an advertisement: people who are interested
in logical relations might like to have a look at a variant
called "prelogical relations" which have most of the useful
properties of logical relations, including the basic lemma,
but which compose, unlike logical relations.  See

@article{prelogical-relations,
	author = {Furio Honsell and Donald Sannella},
	title = {Prelogical Relations},
	journal={Information and Computation},
	year = {2002},
	volume = {178},
	pages = {23--43},
	pdf = {http://homepages.inf.ed.ac.uk/dts/pub/prelogrel-long.pdf}}

(Shorter version in Proc. CSL 1999.)  A categorical version of the
same thing is

@inproceedings{lax-logical-relations,
	author = {Gordon Plotkin and John Power
                 and Donald Sannella and Robert Tennent},
	title = {Lax Logical Relations},
	booktitle = {Proc.\ 27th Intl.\ Colloq.\ on Automata,
                 Languages and Programming},
	location = {Geneva},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	volume = 1853,
	pages = {85--102},
	year = 2000,
	pdf = {http://homepages.inf.ed.ac.uk/dts/pub/laxlogrel.pdf}}

Don Sannella