Verificación estática de contratos sobre tipos de sesión en Haskell

Mostrar todas las versiones(2)

El lenguaje de programación Haskell cuenta con diversas implementaciones de tipos de sesiones binarias. En este trabajo estudiamos la viabilidad de integrarlas con LiquidHaskell, una herramienta de verificación estática que extiende el lenguaje con tipos refinados. Si bien la estructura recursiva de...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autor principal:	Cioppettini, Enzo Samue
Otros Autores:	Melgratti, Hernán Claudio
Formato:	Tesis de grado publishedVersion
Lenguaje:	Español
Publicado:	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2022
Materias:	TIPOS DE SESION TIPOS REFINADOS HASKELL SISTEMAS DE EFECTOS VERIFICACION ESTATICA CONCURRENCIA
Acceso en línea:	https://hdl.handle.net/20.500.12110/seminario_nCOM000553_Cioppettini
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	seminario:seminario_nCOM000553_Cioppettini
record_format	dspace
spelling	seminario:seminario_nCOM000553_Cioppettini2025-08-08T16:50:00Z Verificación estática de contratos sobre tipos de sesión en Haskell Cioppettini, Enzo Samue Melgratti, Hernán Claudio TIPOS DE SESION TIPOS REFINADOS HASKELL SISTEMAS DE EFECTOS VERIFICACION ESTATICA CONCURRENCIA El lenguaje de programación Haskell cuenta con diversas implementaciones de tipos de sesiones binarias. En este trabajo estudiamos la viabilidad de integrarlas con LiquidHaskell, una herramienta de verificación estática que extiende el lenguaje con tipos refinados. Si bien la estructura recursiva de las sesiones se puede codificar fácilmente mediante tipos paramétricos, garantizar tanto la dualidad como el uso linear de los canales requiere de extensiones del lenguaje de mayor complejidad. Nosotros partimos de implementaciones existentes, y que utilizan distintas extensiones y mecanismos. A partir de estas, en la medida en la que son compatibles con LiquidHaskell, exploramos la clase de contratos sobre la comunicación que se pueden escribir y verificar. Para esto utilizamos dos técnicas: una simple de integrar, pero que solo permite escribir contratos sobre cada mensaje, es decir, sin tener en cuenta los valores anteriormente intercambiados; y que permite expresar propiedades más ricas, incluyendo dependencias con los mensajes previos, pero cuya integración es más compleja. Fil: Cioppettini, Enzo Samue. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2022 info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion application/pdf spa info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/seminario_nCOM000553_Cioppettini
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language	Español
orig_language_str_mv	spa
topic	TIPOS DE SESION TIPOS REFINADOS HASKELL SISTEMAS DE EFECTOS VERIFICACION ESTATICA CONCURRENCIA
spellingShingle	TIPOS DE SESION TIPOS REFINADOS HASKELL SISTEMAS DE EFECTOS VERIFICACION ESTATICA CONCURRENCIA Cioppettini, Enzo Samue Verificación estática de contratos sobre tipos de sesión en Haskell
topic_facet	TIPOS DE SESION TIPOS REFINADOS HASKELL SISTEMAS DE EFECTOS VERIFICACION ESTATICA CONCURRENCIA
description	El lenguaje de programación Haskell cuenta con diversas implementaciones de tipos de sesiones binarias. En este trabajo estudiamos la viabilidad de integrarlas con LiquidHaskell, una herramienta de verificación estática que extiende el lenguaje con tipos refinados. Si bien la estructura recursiva de las sesiones se puede codificar fácilmente mediante tipos paramétricos, garantizar tanto la dualidad como el uso linear de los canales requiere de extensiones del lenguaje de mayor complejidad. Nosotros partimos de implementaciones existentes, y que utilizan distintas extensiones y mecanismos. A partir de estas, en la medida en la que son compatibles con LiquidHaskell, exploramos la clase de contratos sobre la comunicación que se pueden escribir y verificar. Para esto utilizamos dos técnicas: una simple de integrar, pero que solo permite escribir contratos sobre cada mensaje, es decir, sin tener en cuenta los valores anteriormente intercambiados; y que permite expresar propiedades más ricas, incluyendo dependencias con los mensajes previos, pero cuya integración es más compleja.
author2	Melgratti, Hernán Claudio
author_facet	Melgratti, Hernán Claudio Cioppettini, Enzo Samue
format	Tesis de grado Tesis de grado publishedVersion
author	Cioppettini, Enzo Samue
author_sort	Cioppettini, Enzo Samue
title	Verificación estática de contratos sobre tipos de sesión en Haskell
title_short	Verificación estática de contratos sobre tipos de sesión en Haskell
title_full	Verificación estática de contratos sobre tipos de sesión en Haskell
title_fullStr	Verificación estática de contratos sobre tipos de sesión en Haskell
title_full_unstemmed	Verificación estática de contratos sobre tipos de sesión en Haskell
title_sort	verificación estática de contratos sobre tipos de sesión en haskell
publisher	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate	2022
url	https://hdl.handle.net/20.500.12110/seminario_nCOM000553_Cioppettini
work_keys_str_mv	AT cioppettinienzosamue verificacionestaticadecontratossobretiposdesesionenhaskell
_version_	1843125984564346880

Verificación estática de contratos sobre tipos de sesión en Haskell

Ejemplares similares