Viktor Vafeiadis: Publications by subject

Items with a check mark () come with a mechanized proof in either Coq or Isabelle/HOL.

See also: [Publications chronologically] [@DBLP] [GoogleScholar]

Weak consistency semantics

Weak memory models

• Making weak memory models fair.
  Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 5, OOPSLA, Article 98 (October 2021)
  Distinguished paper award at OOPSLA'21
  [Paper] [@ACM] [@arXiv] [Artifact @Zenodo]
• Reconciling event structures with modern multiprocessors.
  Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, Viktor Vafeiadis.
  In ECOOP 2020. LIPIcs 166, pp. 5:1-5:26 (June 2020)
  [Paper] [@Dagstuhl] [@arXiV]
• Promising 2.0: Global optimizations in relaxed memory concurrency.
  Sung-Hwan Lee, Minki Cho, Anton Podkopaev, Soham Chakraborty, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis.
  In PLDI 2020, pp. 362–376. ACM (June 2020)
  [Paper] [@ACM] [More...]
• On library correctness under weak memory consistency.
  Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 3, POPL, Article 68 (January 2019)
  [Paper] [@ACM] [More...]
• Bridging the gap between programming languages and hardware weak memory models.
  Anton Podkopaev, Ori Lahav, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 3, POPL, Article 69 (January 2019)
  [Paper] [@ACM] [@arXiv] [More...]
• Grounding thin-air reads with event structures.
  Soham Chakraborty, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 3, POPL, Article 70 (January 2019)
  [Paper] [@ACM] [More...]
• Promising compilation to ARMv8 POP.
  Anton Podkopaev, Ori Lahav, Viktor Vafeiadis.
  In ECOOP 2017, pp. 22:1-22:28 (June 2017)
  [Paper] [@LIPIcs]
• Repairing sequential consistency in C/C++11.
  Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, Derek Dreyer.
  In PLDI 2017, pp. 618-632. ACM (June 2017)
  Distinguished paper award at PLDI'17
  [Paper] [@ACM] [More...]
• Formalizing the concurrency semantics of an LLVM fragment.
  Soham Chakraborty, Viktor Vafeiadis.
  In CGO 2017, pp. 100-110. ACM (February 2017)
  [Paper] [@ACM] [More...]
• A promising semantics for relaxed-memory concurrency.
  Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, Derek Dreyer.
  In POPL 2017, pp. 175-189. ACM (January 2017)
  [Paper] [@ACM] [More...]
• Explaining relaxed memory models with program transformations.
  Ori Lahav, Viktor Vafeiadis.
  In FM 2016. LNCS 9995, pp. 479-495. Springer (November 2016)
  [Paper] [@Springer] [More...]
• Validating optimizations of concurrent C/C++ programs.
  Soham Chakraborty, Viktor Vafeiadis.
  In CGO 2016, pp. 216-226. ACM (March 2016)
  [Paper] [@ACM] [More...]
• Taming release-acquire consistency.
  Ori Lahav, Nick Giannarakis, Viktor Vafeiadis.
  In POPL 2016, pp. 649-662. ACM (January 2016)
  [Paper] [@ACM] [More...]
• Common compiler optimisations are invalid in the C11 memory model and what we can do about it.
  Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli.
  In POPL 2015, pp. 209-220. ACM (January 2015)
  [Paper] [@ACM] [More...]

Transactional and persistence semantics

• Specifying and verifying persistent libraries.
  Leo Stefanesco, Azalea Raad, Viktor Vafeiadis
  In ESOP 2024
  [Paper]
• The Path to Durable Linearizability.
  Emanuele D’Osualdo, Azalea Raad, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 7, POPL, Article 26 (January 2023)
  [Paper] [@ACM]
• The challenges of weak persistency.
  Viktor Vafeiadis.
  In CALCO 2021. LIPIcs 211, pp. 4:1–4:3 (September 2021)
  [Paper] [@Dagstuhl]
• PerSeVerE: Persistency semantics for verification under ext4.
  Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 5, POPL, Article 43 (January 2021)
  [Paper] [@ACM] [More...]
• Persistency semantics of the Intel-x86 architecture.
  Azalea Raad, John Wickerson, Gil Neiger, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 4, POPL, Article 11 (January 2020)
  [Paper] [@ACM] [More...]
• Weak persistency semantics from the ground up: Formalising the persistency semantics of ARMv8 and transactional models.
  Azalea Raad, John Wickerson, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 3, OOPSLA, Article 137 (October 2019)
  [Paper] [@ACM] [More...]
• On the semantics of snapshot isolation.
  Azalea Raad, Ori Lahav, Viktor Vafeiadis.
  In VMCAI 2019 (January 2019)
  [@arXiv] [@Springer]
• Persistence semantics for weak memory: Integrating epoch persistency with the TSO memory model.
  Azalea Raad, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 2, OOPSLA, Article 137 (November 2018)
  [Paper] [@ACM] [More...]
• On parallel snapshot isolation and release/acquire consistency.
  Azalea Raad, Ori Lahav, Viktor Vafeiadis.
  In ESOP 2018. LNCS 10801, pp. 940-967. Springer (April 2018)
  [Paper] [@Springer] [More...]

Verification under weak memory consistency

Program logics

• Persistent Owicki-Gries reasoning: A program logic for reasoning about persistent programs on Intel-x86.
  Azalea Raad, Ori Lahav, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 4, OOPSLA, Article 151 (November 2020)
  [Paper] [@ACM] [More...]
• A separation logic for a promising semantics.
  Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis.
  In ESOP 2018. LNCS 10801, pp. 357-384. Springer (April 2018)
  [Paper] [@Springer] [Technical appendix] [More...]
• Program verification under weak memory consistency using separation logic.
  Viktor Vafeiadis.
  In CAV (1) 2017. LNCS 10426, pp. 30-46. Springer (July 2017)
  [Paper] [@Springer]
• Strong logic for weak memory: Reasoning about release-acquire consistency in Iris.
  Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, Viktor Vafeiadis.
  In ECOOP 2017, pp. 17:1-17:29 (June 2017)
  Best paper award at ECOOP'17
  [Paper] [@LIPIcs] [More...]
• Tackling real-life relaxed concurrency with FSL++.
  Marko Doko, Viktor Vafeiadis.
  In ESOP 2017. LNCS 10201, pp. 448-475. Springer (April 2017)
  [Paper] [@Springer] [More...]
• Reasoning about fences and relaxed atomics.
  Mengda He, Viktor Vafeiadis, Shengchao Qin, João F. Ferreira.
  In PDP 2016, pp. 520-527. IEEE (February 2016)
  [Paper] [@IEEE]
• A program logic for C11 memory fences.
  Marko Doko, Viktor Vafeiadis.
  In VMCAI 2016, LNCS 9583, pp. 413-430. Springer (January 2016)
  [Paper] [@Springer] [More...]
• Owicki-Gries reasoning for weak memory models.
  Ori Lahav, Viktor Vafeiadis.
  In ICALP 2015, Track B. LNCS 9135, pp. 311-323. Springer (July 2015)
  [Paper] [@Springer] [More...]
• Verifying read-copy-update in a logic for weak memory.
  Joseph Tassarotti, Derek Dreyer, Viktor Vafeiadis.
  In PLDI 2015, pp. 110-120, ACM (June 2015)
  [Paper] [@ACM] [More...]
• Formal reasoning about the C11 weak memory model.
  Viktor Vafeiadis.
  In CPP 2015, pp. 1-2. ACM (January 2015)
  [Paper] [@ACM] [Slides]
• GPS: Navigating weak memory with ghosts, protocols, and separation.
  Aaron Turon, Viktor Vafeiadis, Derek Dreyer.
  In OOPSLA 2014, pp. 691-707. ACM (October 2014)
  [Paper] [@ACM] [More...]
• Relaxed separation logic: A program logic for C11 concurrency.
  Viktor Vafeiadis, Chinmay Narayan.
  In OOPSLA 2013, pp. 867-884. ACM (October 2013)
  [Paper] [@ACM] [More...]

Automated verification

• SPORE: Combining symmetry and partial order reduction.
  Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis
  Proc. ACM Program. Lang. 8, PLDI, Article 219 (June 2024)
  [Paper] [More...]
• Enhancing GenMC's usability and performance.
  Michalis Kokologiannakis, Rupak Majumdar, Viktor Vafeiadis
  In TACAS 2024
  [Paper] [More...]
• Optimal bounded partial order reduction.
  Iason Marmanis, Viktor Vafeiadis
  In FMCAD 2023, pp. 86–91 (October 2023)
  [Paper] [@TU Wien]
• Unblocking dynamic partial order reduction.
  Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis
  In CAV 2023, pp. 230-250 (July 2023)
  [Paper] [@Springer] [Appendix] [Artifact @Zenodo]
• BWoS: Formally verified block-based work stealing for parallel processing.
  Jiawei Wang, Bohdan Trach, Ming Fu, Diogo Behrens, Jonathan Schwender, Yutao Liu, Jitang Lei, Viktor Vafeiadis, Hermann Härtig, Haibo Chen
  In OSDI 2023 (July 2023)
  [Paper] [@USENIX]
• AtoMig: Automatically migrating millions lines of code from TSO to WMM.
  Martin Beck, Koustubha Bhat, Lazar Stričević, Geng Chen, Diogo Behrens, Ming Fu, Viktor Vafeiadis, Haibo Chen, Hermann Härtig.
  In ASPLOS 2023 (March 2023)
  [Paper]
• Kater: Automating weak memory model metatheory and consistency checking.
  Michalis Kokologiannakis, Ori Lahav, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 7, POPL, Article 19 (January 2023)
  [Paper] [@ACM] [Artifact @Zenodo]
• SMT-based verification of persistency invariants of Px86 programs.
  Iason Marmanis, Viktor Vafeiadis.
  In VSTTE 2022 (October 2022)
  [Paper]
• Model checking for a multi-execution memory model.
  Evgenii Moiseenko, Michalis Kokologiannakis, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 6, OOPSLA2, Article 152 (October 2022)
  [Paper] [@ACM] [Artifact @Zenodo]
• Truly stateless, optimal dynamic partial order reduction.
  Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 6, POPL, Article 49 (January 2022)
  [Paper] [@ACM] [Artifact @Zenodo]
• Extending Intel-x86 consistency and persistency: Formalising the semantics of Intel-x86 memory types and non-temporal stores.
  Azalea Raad, Luc Maranget, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 6, POPL, Article 22 (January 2022)
  [Paper] [@ACM] [Artifact @Inria]
• Dynamic partial order reductions for spinloops.
  Michalis Kokologiannakis, Xiaowei Ren, Viktor Vafeiadis.
  In FMCAD 2021 (October 2021)
  [Paper] [@IEEE] [More...]
• GenMC: A model checker for weak memory models.
  Michalis Kokologiannakis, Viktor Vafeiadis.
  In CAV 2021 (July 2021)
  [Paper] [@Springer] [Artifact @Zenodo] [More...]
• BAM: Efficient model checking for barriers.
  Michalis Kokologiannakis, Viktor Vafeiadis.
  In NETYS 2021 (May 2021)
  [Paper]
• Verifying and optimizing the HMCS lock for Arm servers.
  Jonas Oberhauser, Lilith Oberhauser, Antonio Paolillo, Diogo Behrens, Ming Fu, Viktor Vafeiadis.
  In NETYS 2021 (May 2021)
  [Paper]
• VSync: Push-button verification and optimization for synchronization primitives on weak memory.
  Jonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, Viktor Vafeiadis.
  In ASPLOS 2021, pp. 530-545. ACM (April 2021)
  Distinguished paper award at ASPLOS'21
  [Paper] [@ACM]
• The decidability of verification under PS 2.0.
  Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, S. Krishna, and Viktor Vafeiadis.
  In ESOP 2021. LNCS 12648, pp. 1-29. Springer (March 2021)
  [Paper] [@Springer]
• HMC: Model checking for hardware memory models.
  Michalis Kokologiannakis, Viktor Vafeiadis.
  In ASPLOS 2020 (March 2020)
  [Paper] [@ACM]
• Effective lock handling in stateless model checking.
  Michalis Kokologiannakis, Azalea Raad, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 3, OOPSLA, Article 173 (October 2019)
  [Paper] [@ACM] [More...]
• Model checking for weakly consistent libraries.
  Michalis Kokologiannakis, Azalea Raad, Viktor Vafeiadis.
  In PLDI 2019, pp. 96-110. ACM (June 2019)
  [Paper] [@ACM] [More...]
• Effective stateless model checking for C/C++ concurrency.
  Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis.
  Proc. ACM Program. Lang. 2, POPL, Article 17 (January 2018)
  [Paper] [@ACM] [More...]

Verification under Sequential consistency

Program logics

• Concurrent separation logic and operational semantics.
  Viktor Vafeiadis.
  In MFPS 2011. ENTCS 276, pp. 335-351. Elsevier (September 2011)
  [Paper] [@Elsevier] [More...]
• Separation logic in the presence of garbage collection.
  Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis.
  In LICS 2011, pp. 247-256. IEEE (June 2011)
  [Paper] [@IEEE] [Technical appendix]
• Concurrent abstract predicates.
  Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew Parkinson, Viktor Vafeiadis.
  In ECOOP 2010. LNCS 6183, pp. 504-528. Springer (June 2010)
  [Paper] [@Springer] [Technical report]
• RGSep action inference.
  Viktor Vafeiadis.
  In VMCAI 2010. LNCS 5944, pp. 345-361. Springer (January 2010)
  [Paper] [@Springer] [Tool (Cave)]
• Structuring the verification of heap-manipulating programs.
  Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine.
  In POPL 2010, pp. 261-273. ACM (January 2010)
  [Paper] [@ACM] [Proof scripts]
• Deny-guarantee reasoning.
  Mike Dodds, Xinyu Feng, Matthew Parkinson, Viktor Vafeiadis.
  In ESOP 2009. LNCS 5502, pp. 363-377. Springer (March 2009)
  [Paper] [@Springer] [Technical report]
• A marriage of rely/guarantee and separation logic.
  Viktor Vafeiadis, Matthew Parkinson.
  In CONCUR 2007. LNCS 4703, pp. 256-271. Springer (September 2007)
  [Paper] [@Springer] [Technical report] [More...]
• Proving correctness of highly-concurrent linearisable objects.
  Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, Marc Shapiro.
  In PPoPP 2006, pp. 129-136. ACM (March 2006)
  [Paper] [@ACM] [Technical report]

Automated verification

• Reconciling preemption bounding with DPOR.
  Iason Marmanis, Michalis Kokologiannakis, Viktor Vafeiadis.
  In TACAS 2023 (April 2023)
  [Paper]
• Rely/guarantee reasoning for asynchronous programs.
  Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, Viktor Vafeiadis.
  In CONCUR 2015, pp. 483-496 (September 2015)
  [Paper] [@LIPIcs]
• Asynchronous liquid separation types.
  Johannes Kloos, Rupak Majumdar, Viktor Vafeiadis.
  In ECOOP 2015, pp. 396-420 (July 2015)
  [Paper] [@LIPIcs] [More...]
• Aspect-oriented linearizability proofs.
  Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis.
  Logical Methods in Computer Science 11(1:20) (March 2015)
  [@LMCS]
• Proving lock-freedom easily and automatically.
  Xiao Jia, Wei Li, Viktor Vafeiadis.
  In CPP 2015, pp. 119-127. ACM (January 2015)
  [Paper] [@ACM] [More...]
• Aspect-oriented linearizability proofs.
  Thomas A. Henzinger, Ali Sezgin, Viktor Vafeiadis.
  In CONCUR 2013. LNCS 8052, pp. 242-256. Springer (August 2013)
  [Paper] [@Springer]
• Automatically proving linearizability.
  Viktor Vafeiadis.
  In CAV 2010. LNCS 6174, pp. 450-464. Springer (July 2010)
  [Paper] [@Springer] [Technical report] [Tool (Cave)]
• Bi-abductive resource invariant synthesis.
  Cristiano Calcagno, Dino Distefano, Viktor Vafeiadis.
  In APLAS 2009. LNCS 5904, pp. 259-274. Springer (December 2009)
  [Paper] [@Springer]
• Proving that nonblocking algorithms don't block.
  Alexey Gotsman, Byron Cook, Matthew Parkinson, Viktor Vafeiadis.
  In POPL 2009, pp. 16-28. ACM (January 2009)
  [Paper] [@ACM]
• Shape-value abstraction for verifying linearizability.
  Viktor Vafeiadis.
  In VMCAI 2009. LNCS 5403, pp. 335-348. Springer (January 2009)
  [Paper] [@Springer] [Tool (Cave)]
• Modular safety checking for fine-grained concurrency.
  Cristiano Calcagno, Matthew Parkinson, Viktor Vafeiadis.
  In SAS 2007. LNCS 4634, pp. 233-238. Springer (August 2007)
  [Paper] [@Springer] [Tool (SmallfootRG)]

Verified compilation

For sequential programs

• Lightweight verification of separate compilation.
  Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis.
  In POPL 2016, pp. 178-190. ACM (January 2016)
  [Paper] [@ACM] [More...]
• Pilsner: A compositionally verified compiler for a higher-order imperative language.
  Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, Viktor Vafeiadis.
  In ICFP 2015, pp. 166-178 (September 2015)
  [Paper] [More...]
• A formal C memory model supporting integer-pointer casts.
  Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis.
  In PLDI 2015, pp. 326-335. ACM (June 2015)
  [Paper] [@ACM] [More...]
• The marriage of bisimulations and Kripke logical relations.
  Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis.
  In POPL 2012, pp. 59-72. ACM (January 2012)
  [Paper] [@ACM] [More...]
• A logical step forward in parametric bisimulations.
  Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.
  Technical report MPI-SWS-2014-003 (January 2014)
  [Paper] [Project page with Coq scripts]
• The transitive composability of relation transition systems.
  Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.
  Technical report MPI-SWS-2012-002 (April 2012)
  [Paper] [Coq scripts]

For concurrent programs

• CompCertTSO: A verified compiler for relaxed-memory concurrency.
  Jaroslav Sevcik, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell.
  J. ACM. 60(3):22 (June 2013)
  [Paper] [@ACM] [More...]
• Verifying fence elimination optimisations.
  Viktor Vafeiadis, Francesco Zappa Nardelli.
  In SAS 2011. LNCS 6887, pp. 146-162. Springer (September 2011)
  [Paper] [@Springer] [More...]
• Relaxed-memory concurrency and verified compilation.
  Jaroslav Sevcik, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell.
  In POPL 2011, pp. 43-54. ACM (January 2011)
  [Paper] [@ACM] [More...]

Other

Interactive theorem proving (Coq)

• Mtac: A monad for typed tactic programming in Coq.
  Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
  J. Functional Programming 25 (August 2015)
  [Paper] [@CUP] [More...]
• Mtac: A monad for typed tactic programming in Coq.
  Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.
  In ICFP 2013, pp. 87-100. ACM (September 2013)
  [Paper] [@ACM] [Implementation (Mtac)]
• Adjustable references.
  Viktor Vafeiadis.
  In ITP 2013. LNCS 7998, pp. 328-337. Springer (July 2013)
  [Paper] [@Springer] [More...]
• The power of parameterization in coinductive proof.
  Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis.
  In POPL 2013, pp. 193-206. ACM (January 2013)
  [Paper] [@ACM] [Coq library (Paco)]

Miscellaneous

• Geo-Replication: Fast If Possible, Consistent If Necessary.
  Valter Balegas, Cheng Li, Mahsa Najafzadeh, Daniel Porto, Allen Clement, Sérgio Duarte, Carla Ferreira, Johannes Gehrke, João Leitão, Nuno M. Preguiça, Rodrigo Rodrigues, Marc Shapiro, Viktor Vafeiadis.
  IEEE Data Engineering Bulletin 39(1): 81-92 (March 2016)
  [@IEEE]
• Modular verification of concurrency-aware linearizability.
  Nir Hemed, Noam Rinetzky, Viktor Vafeiadis.
  In DISC 2015, pp. 371-387 (October 2015)
  [Paper] [@Springer]
• Automating the choices of consistency levels in replicated systems.
  Cheng Li, João Leitão, Allen Clement, Nuno Preguiça, Rodrigo Rodrigues, Viktor Vafeiadis.
  In USENIX ATC 2014, pp. 281-292. USENIX (June 2014)
  [Paper] [@USENIX]
• A programming language approach to fault tolerance for fork-join parallelism.
  Mustafa Zengin, Viktor Vafeiadis.
  In TASE 2013, pp. 105-112. IEEE (July 2013)
  [Paper] [@IEEE] [More...]
• Finding heap-bounds for hardware synthesis.
  Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Jiri Simsa, Satnam Singh, Viktor Vafeiadis.
  In FMCAD 2009, pp. 205-212. IEEE (November 2009)
  [Paper] [@IEEE]
• Acute: High-level programming language design for distributed computation.
  Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis.
  J. Functional Programming 17(4-5): 547-612 (2007)
  [Paper] [@CUP] [More...]
• Acute: High-level programming language design for distributed computation.
  Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis.
  In ICFP 2005, pp. 15-26. ACM (September 2005)
  [Paper] [@ACM] [More...]