Sannella, Donald

Stark, Ian

Katsumata, Shin-ya

2005-11-14T16:13:27Z

2005-11-14T16:13:27Z

2005-07

This thesis proposes a generalisation of pre-logical predicates to simply typed formal systems and their categorical models. We analyse the three elements involved in pre-logical predicates --- syntax, semantics and predicates --- within a categorical framework for typed binding syntax and semantics. We then formulate generalised pre-logical predicates and show two distinguishing properties: a) equivalence with the basic lemma and b) closure of binary pre-logical relations under relational composition. To test the adequacy of this generalisation, we derive pre-logical predicates for various calculi and their categorical models including variations of lambda calculi and non-lambda calculi such as many-sorted algebras as well as first-order logic. We then apply generalised pre-logical predicates to characterising behavioural equivalence. Examples of constructive data refinement of typed formal systems are shown, where behavioural equivalence plays a crucial role in achieving data abstraction.

890216 bytes

application/pdf

http://hdl.handle.net/1842/850

en

University of Edinburgh. College of Science and Engineering. School of Informatics.

Shin-ya Katsumata. A Generalisation of Prelogical Predicates to Simply Typed Formal Systems. In Proc. ICALP 2004. LNCS 3142, pp 831-845. Springer 2004.

Computer Science

Observational Equivalence

Logical Relation

Generalisation of pre-logical predicates and its applications

A generalisation of pre-logical predicates and its applications

Thesis or Dissertation

Doctoral

PhD Doctor of Philosophy