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.
| Main Authors: | , , |
|---|---|
| Format: | conferenceObject |
| Language: | eng |
| Published: |
2025
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/11086/555060 |
| _version_ | 1826514574276296704 |
|---|---|
| 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 |
| collection | Repositorio Digital Universitario |
| description | Ponencia presentada en el 21st Brazilian Symposium on Programming Languages. Fortaleza, Brasil, 21 al 22 de septiembre de 2017. |
| format | conferenceObject |
| id | rdu-unc.555060 |
| institution | Universidad Nacional de Cordoba |
| language | eng |
| publishDate | 2025 |
| record_format | dspace |
| spelling | rdu-unc.5550602025-03-07T15:46:43Z 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 |
| 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 |
| title | 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_short | 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 |
| topic | Computational adequacy Coherence Mechanization |
| 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 |