Treffer: Automating type soundness proofs via decision procedures and guided reductions

Title:
Automating type soundness proofs via decision procedures and guided reductions
Authors:
SYME, Don, GORDON, Andrew D
Source:
LPAR 2002 : logic for programming, artificial intelligence, and reasoning (Tbilisi, 14-18 October 2002)Lecture notes in computer science. :418-434
Publisher Information:
Berlin: Springer, 2002.
Publication Year:
2002
Physical Description:
print, 18 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Mathematics, Mathématiques, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie des langages et analyse syntaxique, Language theory and syntactical analysis, Automatisation, Automation, Automatización, Consistance sémantique, Soundness, Consistencia semantica, Décidabilité, Decidability, Decidibilidad, Interconnexion, Interconnection, Interconexión, Langage JAVA, JAVA language, Lenguaje JAVA, Machine virtuelle, Virtual machine, Máquina virtual
Document Type:
Konferenz Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Microsoft Research, Cambridge, United Kingdom
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=14985289
Rights:
Copyright 2003 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.14985289
Database:
PASCAL Archive

Weitere Informationen

Operational models of fragments of the Java Virtual Machine and the.NET Common Language Runtime have been the focus of considerable study in recent years, and of particular interest have been specifications and machine-checked proofs of type soundness. In this paper we aim to increase the level of automation used when checking type soundness for these formalizations. We present a semi-automated technique for reducing a range of type soundness problems to a form that can be automatically checked using a decidable first-order theory. Deciding problems within this fragment is exponential in theory but is often efficient in practice, and the time required for proof checking can be controlled by further hints from the user. We have applied this technique to two case studies, both of which are type soundness properties for subsets of the.NET CLR. These case studies have in turn aided us in our informal analysis of that system.