2012/11/15 by Pedro Baltazar, Dimitris Mostrous, Vasco T. Vasconcelos · 11 citations
Computer Science · Mathematics · #Algorithm #Computer science #Data type #Formal Methods in Verification #Fragment (logic) #Linear logic #Logic, programming, and type systems #Mathematics #Multiplicative function #Programming language #Protocol (science) #Security and Verification in Computing #Session (web analytics) #Theoretical computer science #Type (biology) #cs.LO
paper · pdf · doi:10.4204/eptcs.101.4
published in Electronic Proceedings in Theoretical Computer Science 101, 38-49 (Open Publishing Association) · In Proceedings LINEARITY 2012, arXiv:1211.3480
openalex publication_date 2012/11/15 · arxiv created 2012/11/17 · arxiv updated 2012/11/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
Session types capture precise protocol structure in concurrent programming, but do not specify properties of the exchanged values beyond their basic type. Refinement types are a form of dependent types that can address this limitation, combining types with logical formulae that may refer to program values and can constrain types using arbitrary predicates. We present a pi calculus with assume and assert operations, typed using a session discipline that incorporates refinement formulae written in a fragment of Multiplicative Linear Logic. Our original combination of session and refinement types, together with the well established benefits of linearity, allows very fine-grained specifications of communication protocols in which refinement formulae are treated as logical resources rather than persistent truths.