CINECA IRIS Institutional Research Information System
IRIS è il sistema di gestione integrata dei dati della ricerca (persone, progetti, pubblicazioni, attività) adottato dall'Università degli Studi di Torino.
AperTO è l'archivio istituzionale Open Access destinato a raccogliere, rendere visibile e conservare la produzione scientifica dell'Università degli Studi di Torino.
EnglishWe propose a novel general approach for defining expressive type systems for object-oriented languages, based on abstract compilation of programs into coinductive constraint logic programs defined on a specific constraint domain X called type domain. In this way, type checking and type inference amount to resolving a certain goal w.r.t. the coinductive (that is, the greatest) Herbrand model of a logic program (that is, a Horn formula) with constraints over a fixed type domain X. In particular, we show an interesting instantiation where the constraint predicates of X are syntactic equality and subtyping over coinductive object and union types. The corresponding type system is so expressive to allow verification of simple properties like data structure invariants. Finally, we show a prototype implementation, written in Prolog, of the inference engine for coinductive CLP(X), which is parametric in the solver for the type domain X.
| Titolo: | Abstract compilation of object-oriented languages into coinductive CLP(X): when type inference meets verification |
| Autori Riconosciuti: | |
| Autori: | Davide Ancona; Andrea Corradi; Giovanni Lagorio; Ferruccio Damiani |
| Data di pubblicazione: | 2010 |
| Abstract: | We propose a novel general approach for defining expressive type systems for object-oriented languages, based on abstract compilation of programs into coinductive constraint logic programs defined on a specific constraint domain X called type domain. In this way, type checking and type inference amount to resolving a certain goal w.r.t. the coinductive (that is, the greatest) Herbrand model of a logic program (that is, a Horn formula) with constraints over a fixed type domain X. In particular, we show an interesting instantiation where the constraint predicates of X are syntactic equality and subtyping over coinductive object and union types. The corresponding type system is so expressive to allow verification of simple properties like data structure invariants. Finally, we show a prototype implementation, written in Prolog, of the inference engine for coinductive CLP(X), which is parametric in the solver for the type domain X. |
| Editore: | Fakultät für Informatik (Fak. f. Informatik) Institut für Theoretische Informatik (ITI) |
| Titolo del libro: | Formal Verification of Object-Oriented Software. Papers presented at the International Conference, June 28-30, 2010, Paris, France |
| Volume: | 13 |
| Pagina iniziale: | 330 |
| Pagina finale: | 344 |
| Nome del convegno: | International Conference Formal Verification of Object-Oriented Software 2010 |
| Luogo del convegno: | Paris, France |
| Anno del convegno: | June 28-30, 2010 |
| URL: | http://digbib.ubka.uni-karlsruhe.de/volltexte/1000019083 |
| Parole Chiave: | Object-oriented languages; coinductive constraint logic programming; Prolog |
| Appare nelle tipologie: | 04A-Conference paper in volume |
File in questo prodotto:
Copyright © 2019