dc.contributor.author | Koutavas, Vasileios | |
dc.contributor.author | Lin Hou, Yu | |
dc.date.accessioned | 2023-09-11T06:26:58Z | |
dc.date.available | 2023-09-11T06:26:58Z | |
dc.date.created | 26-29 June 2023 | en |
dc.date.issued | 2023 | |
dc.date.submitted | 2023 | en |
dc.identifier.citation | Vasileios Koutavas; Yu-Yang Lin; Nikos Tzevelekos, Fully Abstract Normal Form Bisimulation for Call-by-Value PCF, 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Boston, MA, USA, 26-29 June 2023, IEEE, 2023, 1 - 13 | en |
dc.identifier.other | Y | |
dc.identifier.uri | http://hdl.handle.net/2262/103829 | |
dc.description.abstract | We present the first fully abstract normal form
bisimulation for call-by-value PCF (PCFv). Our model is based
on a labelled transition system (LTS) that combines elements from
applicative bisimulation, environmental bisimulation and game
semantics. In order to obtain completeness while avoiding the use
of semantic quotiening, the LTS constructs traces corresponding to
interactions with possible functional contexts. The model gives rise
to a sound and complete technique for checking of PCFv program
equivalence, which we implement in a bounded bisimulation
checking tool. We test our tool on known equivalences from the
literature and new examples. | en |
dc.format.extent | 1 | en |
dc.format.extent | 13 | en |
dc.language.iso | en | en |
dc.publisher | IEEE | en |
dc.rights | Y | en |
dc.subject | PCF, Biosimulation | en |
dc.title | Fully Abstract Normal Form Bisimulation for Call-by-Value PCF | en |
dc.title.alternative | 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) | en |
dc.title.alternative | 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) | en |
dc.type | Conference Paper | en |
dc.type.supercollection | scholarly_publications | en |
dc.type.supercollection | refereed_publications | en |
dc.identifier.peoplefinderurl | http://people.tcd.ie/vkoutav | |
dc.identifier.peoplefinderurl | http://people.tcd.ie/linhouy | |
dc.identifier.rssinternalid | 258371 | |
dc.identifier.doi | http://dx.doi.org/10.1109/LICS56636.2023.10175778 | |
dc.rights.ecaccessrights | openAccess | |
dc.subject.TCDTag | Computer Programming Languages | en |
dc.subject.TCDTag | Formal (i.e. mathematical) Methods In Computer Science | en |
dc.subject.TCDTag | Formal Methods | en |
dc.subject.TCDTag | Formal Semantics | en |
dc.subject.TCDTag | Program Equivalence | en |
dc.subject.TCDTag | Program Verification | en |
dc.identifier.orcid_id | 0000-0002-3970-2486 | |
dc.status.accessible | N | en |
dc.contributor.sponsor | Science Foundation Ireland (SFI) | en |
dc.contributor.sponsorGrantNumber | 13/RC/2094_2 | en |