Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/89615
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Dahlqvist, Fredrik | por |
dc.contributor.author | Neves, Renato Jorge Araújo | por |
dc.date.accessioned | 2024-03-16T13:26:42Z | - |
dc.date.available | 2024-03-16T13:26:42Z | - |
dc.date.issued | 2023 | - |
dc.identifier.citation | Dahlqvist, F., & Neves, R. (2023, November 23). A Complete V-Equational System for Graded lambda-Calculus. Electronic Notes in Theoretical Informatics and Computer Science. Episciences.org. http://doi.org/10.46298/entics.12299 | por |
dc.identifier.issn | 2969-2431 | - |
dc.identifier.uri | https://hdl.handle.net/1822/89615 | - |
dc.description.abstract | Modern programming frequently requires generalised notions of program equivalence based on a metric or a similar structure. Previous work addressed this challenge by introducing the notion of a V-equation, i.e. an equation labelled by an element of a quantale V, which covers inter alia (ultra-)metric, classical, and fuzzy (in)equations. It also introduced a V-equational system for the linear variant of lambda-calculus where any given resource must be used exactly once. In this paper we drop the (often too strict) linearity constraint by adding graded modal types which allow multiple uses of a resource in a controlled manner. We show that such a control, whilst providing more expressivity to the programmer, also interacts more richly with V-equations than the linear or Cartesian cases. Our main result is the introduction of a sound and complete V-equational system for a lambda-calculus with graded modal types interpreted by what we call a Lipschitz exponential comonad. We also show how to build such comonads canonically via a universal construction, and use our results to derive graded metric equational systems (and corresponding models) for programs with timed and probabilistic behaviour. | por |
dc.description.sponsorship | This work is financed by National Funds through FCT - Fundação para a Ciência e a Tecnologia, I.P. (Portuguese Foundation for Science and Technology) within project IBEX, with reference PTDC/CCI-COM/4280/2021. | por |
dc.language.iso | eng | por |
dc.publisher | Episciences.org | por |
dc.relation | info:eu-repo/grantAgreement/FCT/3599-PPCDT/PTDC%2FCCI-COM%2F4280%2F2021/PT | por |
dc.rights | openAccess | por |
dc.rights.uri | http://creativecommons.org/licenses/by/4.0/ | por |
dc.subject | λ-calculus | por |
dc.subject | graded modal type | por |
dc.subject | quantitative equational theory | por |
dc.subject | enriched category theory | por |
dc.title | A complete V-equational system for graded lambda-calculus | por |
dc.type | conferencePaper | por |
dc.peerreviewed | yes | por |
dc.relation.publisherversion | https://entics.episciences.org/12299 | por |
oaire.citationVolume | 3 | por |
dc.identifier.doi | 10.46298/entics.12299 | por |
dc.subject.fos | Ciências Naturais::Ciências da Computação e da Informação | por |
sdum.journal | Electronic Notes in Theoretical Informatics and Computer Science | por |
sdum.conferencePublication | 39th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIX) | por |
oaire.version | VoR | por |
Aparece nas coleções: | DI/CCTC - Artigos (papers) |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
neves23.pdf | 375,09 kB | Adobe PDF | Ver/Abrir |
Este trabalho está licenciado sob uma Licença Creative Commons