The importance of being extrinsic : coherence and adequacy for a call-by-value language

Ponencia presentada en el 21st Brazilian Symposium on Programming Languages. Fortaleza, Brasil, 21 al 22 de septiembre de 2017.

Guardado en:
Detalles Bibliográficos
Autores principales: Gadea, Alejandro Emilio, Gunther, Emmanuel, Pagano, Miguel María
Formato: conferenceObject
Lenguaje:Inglés
Publicado: 2025
Materias:
Computational adequacy
Coherence
Mechanization
Acceso en línea:http://hdl.handle.net/11086/555060
Aporte de:
Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba
id I10-R141-11086-555060
record_format dspace
spelling I10-R141-11086-5550602025-03-12T14:50:52Z The importance of being extrinsic : coherence and adequacy for a call-by-value language Gadea, Alejandro Emilio Gunther, Emmanuel Pagano, Miguel María Computational adequacy Coherence Mechanization Ponencia presentada en el 21st Brazilian Symposium on Programming Languages. Fortaleza, Brasil, 21 al 22 de septiembre de 2017. Fil: Gadea, Alejandro Emilio. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Fil: Gadea, Alejandro Emilio. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Fil: Gunther, Emmanuel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Fil: Gunther, Emmanuel. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Fil: Pagano, Miguel María. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. In this paper we mechanize in Coq a typed, call-by-value language by specifying its operational semantics and giving intrinsic and extrinsic denotational semantics, both using domain theory. We also prove that the denotational semantics are equivalent; this is interesting because it leads to a direct proof of coherence for the intrinsic semantics. Finally, we prove the adequacy of the operational semantics with respect to the denotational semantics. As far as we know, this is the first mechanization of Reynolds’ bracketing theorem and also the use of biorthogonality with extrinsic semantics instead of intrinsic semantics. Fil: Gadea, Alejandro Emilio. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Fil: Gadea, Alejandro Emilio. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Fil: Gunther, Emmanuel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Fil: Gunther, Emmanuel. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Fil: Pagano, Miguel María. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Ciencias de la Computación 2025-03-07T14:42:20Z 2025-03-07T14:42:20Z 2017 conferenceObject 978-1-4503-5389-2 http://hdl.handle.net/11086/555060 eng Atribución/Reconocimiento-NoComercial-SinDerivados 4.0 Internacional http://creativecommons.org/licenses/by-nc-nd/4.0/deed.es Electrónico y/o Digital
institution Universidad Nacional de Córdoba
institution_str I-10
repository_str R-141
collection Repositorio Digital Universitario (UNC)
language Inglés
topic Computational adequacy
Coherence
Mechanization
spellingShingle Computational adequacy
Coherence
Mechanization
Gadea, Alejandro Emilio
Gunther, Emmanuel
Pagano, Miguel María
The importance of being extrinsic : coherence and adequacy for a call-by-value language
topic_facet Computational adequacy
Coherence
Mechanization
description Ponencia presentada en el 21st Brazilian Symposium on Programming Languages. Fortaleza, Brasil, 21 al 22 de septiembre de 2017.
format conferenceObject
author Gadea, Alejandro Emilio
Gunther, Emmanuel
Pagano, Miguel María
author_facet Gadea, Alejandro Emilio
Gunther, Emmanuel
Pagano, Miguel María
author_sort Gadea, Alejandro Emilio
title The importance of being extrinsic : coherence and adequacy for a call-by-value language
title_short The importance of being extrinsic : coherence and adequacy for a call-by-value language
title_full The importance of being extrinsic : coherence and adequacy for a call-by-value language
title_fullStr The importance of being extrinsic : coherence and adequacy for a call-by-value language
title_full_unstemmed The importance of being extrinsic : coherence and adequacy for a call-by-value language
title_sort importance of being extrinsic : coherence and adequacy for a call-by-value language
publishDate 2025
url http://hdl.handle.net/11086/555060
work_keys_str_mv AT gadeaalejandroemilio theimportanceofbeingextrinsiccoherenceandadequacyforacallbyvaluelanguage
AT guntheremmanuel theimportanceofbeingextrinsiccoherenceandadequacyforacallbyvaluelanguage
AT paganomiguelmaria theimportanceofbeingextrinsiccoherenceandadequacyforacallbyvaluelanguage
AT gadeaalejandroemilio importanceofbeingextrinsiccoherenceandadequacyforacallbyvaluelanguage
AT guntheremmanuel importanceofbeingextrinsiccoherenceandadequacyforacallbyvaluelanguage
AT paganomiguelmaria importanceofbeingextrinsiccoherenceandadequacyforacallbyvaluelanguage
_version_ 1827088575796084736

Ejemplares similares