Five papers by IMDEA Software Institute researchers have been accepted for publication at the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014), a top-ranked conference in the area of programming languages and systems.

• IMDEA Software faculty members Gilles Barthe and Pierre-Yves Strub have a paper on probabilistic relational verification for cryptographic implementations, together with Cédric Fournet, Nikhil Swamy and Santiago Zanella-Béguelin (Microsoft Research), and Benjamin Grégoire (INRIA).

• Another paper by Pierre-Yves Strub is on gradual typing securely embedded in JavaScript, with Karthikeyan Bhargavan (INRIA), Gavin Bierman, Juan Chen, Cédric Fournet and Nikhil Swamy (Microsoft Research), and Aseem Rastogi (University of Maryland and Microsoft Research).

• IMDEA Software faculty member Alexey Gotsman has a paper on specification, verification and optimality of replicated data types, with Sebastian Burckhardt (Microsoft Research), Hongseok Yang (University of Oxford), and Marek Zawirski (INRIA and UPMC-LIP6).

• IMDEA Software faculty members Anindya Banerjee and Aleks Nanevski have a paper on modular reasoning on heap paths via effectively propositional formulas, with Shachar Itzhaky, Ori Lahav and Mooly Sagiv (Tel Aviv University), and Neil Immerman (University of Massachusetts).

• IMDEA Software postdoctoral researcher Ilya Sergey has a paper on theory and practice of higher-order cardinality analysis, with Dimitrios Vytiniotis and Simon Peyton Jones (Microsoft Research).

These five papers are among 51 papers selected for publication out of 220 submissions to the conference.