Logical Equivalence for Subtyping Object and Recursive Types |
| |
| Authors: | Steffen van Bakel Ugo de’Liguoro |
| |
| Affiliation: | (1) Department of Computing, Imperial College, 180 Queen’s Gate, London, SW7 2BZ, UK;(2) Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149 Torino, Italy |
| |
| Abstract: | Subtyping in first order object calculi is studied with respect to the logical semantics obtained by identifying terms that satisfy the same set of predicates, as formalised through an assignment system. It is shown that equality in the full first order ς-calculus is modelled by this notion, which in turn is included in a Morris-style contextual equivalence. U. de’Liguoro’s research was partially supported by project PRIN’05 prot. 2005015785_003. |
| |
| Keywords: | Object calculi Type theory Program logic |
| 本文献已被 SpringerLink 等数据库收录！ |
|
