Observatorio de I+D+i UPM

Memorias de investigación
Ponencias en congresos:
A Practical Type Analysis for Verification of Modular Prolog Programs
Áreas de investigación
  • Lenguaje de programación
Regular types are a powerful tool for computing very precise descriptive types for logic programs. However, in the context of reallife, modular Prolog programs, the accurate results obtained by regular types often come at the price of efficiency. In this paper we propose a combination of techniques aimed at improving analysis efficiency in this context. As a first technique we allow optionally reducing the accuracy of inferred types by using only the types defined by the user or present in the libraries. We claim that, for the purpose of verifying type signatures given in the form of assertions the precision obtained using this approach is sufficient, and show that analysis times can be reduced significantly. Our second technique is aimed at dealing with situations where we would like to limit the amount of reanalysis performed, especially for library modules. Borrowing some ideas from polymorphic type systems, we show how to solve the problem by admitting parameters in type specifications. This allows us to compose new call patterns with some precomputed analysis info without losing any information. We argue that together these two techniques contribute to the practical and scalable analysis and verification of types in Prolog programs.
Nombre congreso
Workshop on Partial Evaluation and Program Manipulation (PEPM'08)
Tipo de participación
Lugar del congreso
San Francisco, USA
Fecha inicio congreso
Fecha fin congreso
Desde la página
Hasta la página
Título de las actas
A Practical Type Analysis for Verification of Modular Prolog Programs
Esta actividad pertenece a memorias de investigación
  • Autor: Pawel Stanislaw Pietrzak . (UPM)
  • Autor: Manuel de Hermenegildo Salinas (UPM)
  • Autor: Jesus Correas Fernandez (UPM)
  • Autor: Alvaro German Puebla Sanchez (UPM)
Grupos de investigación, Departamentos, Centros e Institutos de I+D+i relacionados
  • Creador: Grupo de Investigación: Computación lógica, Lenguajes, Implementación y Paralelismo (CLIP)
  • Departamento: Lenguajes y Sistemas Informáticos e Ingeniería de Software
  • Departamento: Inteligencia Artificial
S2i 2023 Observatorio de investigación @ UPM con la colaboración del Consejo Social UPM
Cofinanciación del MINECO en el marco del Programa INNCIDE 2011 (OTR-2011-0236)
Cofinanciación del MINECO en el marco del Programa INNPACTO (IPT-020000-2010-22)