Proyecto de Investigación "Fondo Clemente Estable" Nro. 4112.

Subtipos y Objetos en Teorías y Herramientas de Programación
Basadas en Teoría de Tipos.
 

Propuesta del proyecto.

El resumen del area de investigación, antecedentes del equipo de investigación, los objetivos del proyecto y la metodología de trabajo son detallados en el documento de propuesta del proyecto.

Publicaciones

Revistas científicas internacionales con referato

G. Betarte. Type Checking Dependent (Record) Types and Subtyping.
In Journal of Functional Programming, volume 10(2), 137-166, March 2000.

G. Betarte, C. Cornes, N. Szasz, A. Tasistro. Specification of a Smart Card Operating System.
Lecture Notes in Computer Science No. 1956 - Types for Proofs and Programs, pp. 77-93, Springer Verlag, 2000.

Conferencias Internacionales con referato

D. Perovich, L. Rodríguez, M. Varela. A Simple Methodology for Secure Object Sharing.
Gemplus Developer Conference, Paris, France, 2001

Tesis de grado

Las siguientes son tesis de grado que fueron supervisadas por miembros del proyecto y cuya temática esta relacionada directa o indirectamente con los temas de investigación abordados en el mismo.

Programación en Java Card.
D. Perovich, L. Rodriguez, M. Varela. Tesis de grado de la carrera Ingeniero en Computación, 2000.
Supervisor: G. Betarte.

Especificación Formal de la Máquina Virtual Java Card.
L. Grandillo, J. Erlich. Tesis de grado de la carrera Ingeniero en Computación, 2000.
Supervisores: G. Betarte, A. Pardo.

Semántica Formal de un subconjunto de Java.
M. Saez, R. Zerpa. Tesis de grado de la carrera Ingeniero en Computación, 2000.
Supervisores: G. Betarte, A. Pardo.

Software

SubRec: un verificador para Teoría de Tipos de Martin-Loef extendida con Registros Dependientes y Subtipos.

SubRec es un verificador para Teoría de Tipos de Martin-Loef extendida con Registros Dependientes y Subtipos. Este verificador provee además la posibilidad de definir familias de tipos y expresiones let y use . Una muy simple interfase XEmacs ha sido implementada para facilitar la edición de pruebas usando el verificador.

Distribución de SubRec

Un paper que describe el uso de SubRec para la formalización de Algebra abstracta

FOb: un intérprete para un lenguaje Orientado a Objetos basado en objetos.

FOb es un intérprete para un lenguaje orientado a objetos basado en objetos y funcional. El intérprete implementa básicamente el algoritmo de reducción definido para los términos cerrados del cálculo Sigma presentado en el libro "A Theory of Objects" de M. Abadi y L. Cardelli. Este cálculo provee un marco formal y preciso para la definición de construcciones básicas de los lenguajes de programación orientados a objetos.

Una breve descripción del intérprete esta disponible en  resumen

Transparencias de la ponencia Interpretando Objetos (archivo PowerPoint),  presentada en las  "V Jornadas de Informática e Investigación Operativa" (InCo, Montevideo, 2000).

Codigo fuente (Haskell) del intérprete, modo Emacs para la edición y ejecución de programas FOb y help del sistema fob.tar.gz .

Implementación Java de FOb (desarrollada por A. Vignaga) JavaFOb