ACM DL

Programming Languages and Systems (TOPLAS)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 36 Issue 1, March 2014

Extending Type Inference to Variational Programs
Sheng Chen, Martin Erwig, Eric Walkingshaw
Article No.: 1
DOI: 10.1145/2518190

Through the use of conditional compilation and related tools, many software projects can be used to generate a huge number of related programs. The problem of typing such variational software is difficult. The brute-force strategy of generating...

Æminium: A Permission-Based Concurrent-by-Default Programming Language Approach
Sven Stork, Karl Naden, Joshua Sunshine, Manuel Mohr, Alcides Fonseca, Paulo Marques, Jonathan Aldrich
Article No.: 2
DOI: 10.1145/2543920

Writing concurrent applications is extremely challenging, not only in terms of producing bug-free and maintainable software, but also for enabling developer productivity. In this article we present the Æminium concurrent-by-default...

Rely-Guarantee-Based Simulation for Compositional Verification of Concurrent Program Transformations
Hongjin Liang, Xinyu Feng, Ming Fu
Article No.: 3
DOI: 10.1145/2576235

Verifying program transformations usually requires proving that the resulting program (the target) refines or is equivalent to the original one (the source). However, the refinement relation between individual sequential threads cannot be...

Formal Verification of an SSA-Based Middle-End for CompCert
Gilles Barthe, Delphine Demange, David Pichardie
Article No.: 4
DOI: 10.1145/2579080

CompCert is a formally verified compiler that generates compact and efficient code for a large subset of the C language. However, CompCert foregoes using SSA, an intermediate representation employed by many compilers that enables writing simpler,...