JournalTOCs

ACM Transactions on Programming Languages and Systems (TOPLAS)
Journal Prestige (SJR): 0.533

Citation Impact (citeScore): 3
Number of Followers: 18

Hybrid journal (It can contain Open Access articles)
ISSN (Print) 0164-0925 - ISSN (Online) 1558-4593
Published by ACM

[83 journals]

Armed Cats: Formal Concurrency Modelling at Arm
- Free pre-print version: Loading...
  Rate this result: What is this?
  
  Please help us test our new pre-print finding feature by giving the pre-print link a rating.
  A 5 star rating indicates the linked pre-print has the exact same content as the published article.
  
  Abstract: Jade Alglave, Will Deacon, Richard Grisenthwaite, Antoine Hacquard, Luc Maranget
  
  We report on the process for formal concurrency modelling at Arm. An initial formal consistency model of the Arm achitecture, written in the cat language, was published and upstreamed to the herd+diy tool suite in 2017. Since then, we have extended the original model with extra features, for example, mixed-size accesses, and produced two provably equivalent alternative formulations. In this article, we present a comprehensive review of work done at Arm on the consistency model. Along the way, we also show that our principle for handling mixed-size accesses applies to x86: We confirm this via vast experimental campaigns.
  PubDate: Fri, 23 Jul 2021 00:00:00 GMT
On Polymorphic Sessions and Functions: A Tale of Two (Fully Abstract)
Encodings
- Free pre-print version: Loading...
  Rate this result: What is this?
  
  Please help us test our new pre-print finding feature by giving the pre-print link a rating.
  A 5 star rating indicates the linked pre-print has the exact same content as the published article.
  
  Abstract: Bernardo Toninho, Nobuko Yoshida
  
  This work exploits the logical foundation of session types to determine what kind of type discipline for the Λ-calculus can exactly capture, and is captured by, Λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F.
  PubDate: Thu, 10 Jun 2021 00:00:00 GMT
Ranking and Repulsing Supermartingales for Reachability in Randomized
Programs
- Free pre-print version: Loading...
  Rate this result: What is this?
  
  Please help us test our new pre-print finding feature by giving the pre-print link a rating.
  A 5 star rating indicates the linked pre-print has the exact same content as the published article.
  
  Abstract: Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, Ichiro Hasuo
  
  Computing reachability probabilities is a fundamental problem in the analysis of randomized programs. This article aims at a comprehensive and comparative account of various martingale-based methods for over- and under-approximating reachability probabilities. Based on the existing works that stretch across different communities (formal verification, control theory, etc.), we offer a unifying account. In particular, we emphasize the role of order-theoretic fixed points—a classic topic in computer science—in the analysis of randomized programs. This leads us to two new martingale-based techniques, too. We also make an experimental comparison using our implementation of template-based synthesis algorithms for those martingales.
  PubDate: Tue, 08 Jun 2021 00:00:00 GMT
A Programming Language for Data Privacy with Accuracy Estimations
- Free pre-print version: Loading...
  Rate this result: What is this?
  
  Please help us test our new pre-print finding feature by giving the pre-print link a rating.
  A 5 star rating indicates the linked pre-print has the exact same content as the published article.
  
  Abstract: Elisabet Lobo-Vesga, Alejandro Russo, Marco Gaboardi
  
  Differential privacy offers a formal framework for reasoning about the privacy and accuracy of computations on private data. It also offers a rich set of building blocks for constructing private data analyses. When carefully calibrated, these analyses simultaneously guarantee the privacy of the individuals contributing their data, and the accuracy of the data analysis results, inferring useful properties about the population. The compositional nature of differential privacy has motivated the design and implementation of several programming languages to ease the implementation of differentially private analyses. Even though these programming languages provide support for reasoning about privacy, most of them disregard reasoning about the accuracy of data analyses.
  PubDate: Tue, 08 Jun 2021 00:00:00 GMT
ACM Transactions on Programming Languages and Systems (TOPLAS) Volume 43
Issue 2, June 2021 (Issue-in-Progress)
- Free pre-print version: Loading...
  Rate this result: What is this?
  
  Please help us test our new pre-print finding feature by giving the pre-print link a rating.
  A 5 star rating indicates the linked pre-print has the exact same content as the published article.
  
  PubDate: Tue, 01 Jun 2021 00:00:00 GMT