tailieunhanh - Types for Proofs and Programs

We propose a novel approach to constraint-based type inference based on coinductive logic. Constraint generation corresponds to translation into a conjunction of Horn clauses P, and constraint satisfaction is defined in terms of the coinductive Herbrand model of P. We illustrate the approach by formally defining this translation for a small object-oriented language similar to Featherweight Java, where type annotations in field and method declarations can be omitted. In this way, we obtain a very precise type inference and provide new insights into the challenging problem of type inference for object-oriented programs. Since the approach is deliberately declarative, we define in fact a formal specification for a general class of. | Lecture Notes in Computer Science 5497 Commenced Publication in 1973 Founding and Former Series Editors Gerhard Goos Juris Hartmanis and Jan van Leeuwen Editorial Board David Hutchison Lancaster University UK Takeo Kanade Carnegie Mellon University Pittsburgh PA USA Josef Kittler University of Surrey Guildford UK Jon M. Kleinberg Cornell University Ithaca NY USA Alfred Kobsa University of California Irvine CA USA Friedemann Mattern ETH Zurich Switzerland John C. Mitchell Stanford University CA USA Moni Naor Weizmann Institute of Science Rehovot Israel Oscar Nierstrasz University of Bern Switzerland C. Pandu Rangan Indian Institute of Technology Madras India Bernhard Steffen University of Dortmund Germany Madhu Sudan Massachusetts Institute of Technology MA USA Demetri Terzopoulos University of California Los Angeles CA USA Doug Tygar University of California Berkeley CA USA Gerhard Weikum Max-Planck Institute of Computer Science Saarbruecken Germany Stefano Berardi Ferruccio Damiani Ugo de Liguoro Eds. Types for Proofs and Programs International Conference TYPES 2008 Torino Italy March 26-29 2008 Revised Selected Papers 1 Springer Volume Editors Stefano Berardi Ferruccio Damiani Ugo de Liguoro Università di Torino Dipartimento di Informatica Corso Svizzera 185 10149 Torino Italy E-mail stefano damiani deligu @ Library of Congress Control Number Applied for CR Subject Classification 1998 LNCS Sublibrary SL 1 - Theoretical Computer Science and General Issues ISSN 0302-9743 ISBN-10 3-642-02443-2 Springer Berlin Heidelberg New York ISbN-13 978-3-642-02443-6 Springer Berlin Heidelberg New York This work is subject to copyright. All rights are reserved whether the whole or part of the material is concerned specifically the rights of translation reprinting re-use of illustrations recitation broadcasting reproduction on microfilms or in any other way and storage in data banks. Duplication of this publication or parts thereof is permitted