Treffer: Infinitary Refinement Types for Temporal Properties in Scott Domains
Title:
Infinitary Refinement Types for Temporal Properties in Scott Domains
Authors:
Contributors:
Preuves et Langages (PLUME), Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon), Université de Lyon-Université de Lyon-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon), Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Dexter Kozen, Ruy de Queiroz, ANR-20-CE48-0005,QuaReMe,Méthodes de raisonnement quantitative pour les logiques probabilistiques(2020)
Source:
Lecture Notes in Computer Science ; Logic, Language, Information, and Computation ; https://hal.science/hal-05285182 ; Logic, Language, Information, and Computation, Jul 2025, Porto, Portugal. pp.175-193, ⟨10.1007/978-3-031-99536-1_11⟩
Publisher Information:
CCSD
Springer Nature Switzerland
Springer Nature Switzerland
Publication Year:
2025
Collection:
HAL Lyon 1 (University Claude Bernard Lyon 1)
Subject Terms:
Temporal Logic, Scott Domains, Refinement TYpes, ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs, ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.2: Semantics of Programming Languages, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic, [INFO]Computer Science [cs]
Time:
Porto, Portugal
Document Type:
Konferenz
conference object
Language:
English
Relation:
info:eu-repo/semantics/altIdentifier/arxiv/2502.11917; ARXIV: 2502.11917
DOI:
10.1007/978-3-031-99536-1_11
Accession Number:
edsbas.E30AD048
Database:
BASE
Weitere Informationen
International audience ; We discuss an infinitary refinement type system for input- output temporal specifications of functions that handle infinite objects like streams or infinite trees. Our system is based on a reformulation of Bonsangue and Kok’s infinitary extension of Abramsky’s Domain Theory in Logical Form to saturated properties. We show that in an interesting range of cases, our system is complete without the need of an infinitary rule introduced by Bonsangue and Kok to reflect the well-filteredness of Scott domains.