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 https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000553_Cioppettini_oai
Aporte de:	Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires

id	I28-R145-seminario_nCOM000553_Cioppettini_oai
record_format	dspace
spelling	I28-R145-seminario_nCOM000553_Cioppettini_oai2025-08-20 Melgratti, Hernán Claudio Cioppettini, Enzo Samue 2022 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. application/pdf https://hdl.handle.net/20.500.12110/seminario_nCOM000553_Cioppettini spa Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar TIPOS DE SESION TIPOS REFINADOS HASKELL SISTEMAS DE EFECTOS VERIFICACION ESTATICA CONCURRENCIA Verificación estática de contratos sobre tipos de sesión en Haskell info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000553_Cioppettini_oai
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-145
collection	Repositorio Digital de la Universidad de Buenos Aires (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 https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000553_Cioppettini_oai
work_keys_str_mv	AT cioppettinienzosamue verificacionestaticadecontratossobretiposdesesionenhaskell
_version_	1843126914894528512

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

Ejemplares similares