@inproceedings(DBLP:journals/corr/abs-1302-6331, author = {Marco Carbone and Fabrizio Montesi}, year = {2012}, title = {Merging Multiparty Protocols in Multiparty Choreographies}, booktitle = {PLACES}, series = {{EPTCS}}, volume = {109}, pages = {21--27}, doi = {10.4204/EPTCS.109.4}, ) @article(formal-verification-mpi, author = {Ganesh Gopalakrishnan and Robert M. Kirby and Stephen F. Siegel and Rajeev Thakur and William Gropp and Ewing L. Lusk and Bronis R. de Supinski and Martin Schulz and Greg Bronevetsky}, year = {2011}, title = {Formal Analysis of {MPI}-based Parallel Programs}, journal = {Communications of the ACM}, volume = {54}, number = {12}, pages = {82--91}, doi = {10.1145/2043174.2043194}, ) @book(Gropp:1999:UMP:330577, author = {William Gropp and Ewing Lusk and Anthony Skjellum}, year = {1999}, title = {Using MPI (2nd Ed.): Portable Parallel Programming with the Message-passing Interface}, publisher = {MIT Press}, ) @techreport(brinch:1991, author = {Per Brinch Hansen}, year = {1991}, title = {The N-Body Pipeline}, type = {Electrical Engineering and Computer Science Technical Reports}, number = {Paper 120}, institution = {College of Engineering and Computer Science, Syracuse University}, ) @article(DBLP:journals/jacm/HondaYC16, author = {Kohei Honda and Nobuko Yoshida and Marco Carbone}, year = {2016}, title = {Multiparty Asynchronous Session Types}, journal = {J. {ACM}}, volume = {63}, number = {1}, pages = {9:1--9:67}, doi = {10.1145/2827695}, ) @inproceedings(DBLP:journals/corr/LangeS13, author = {Julien Lange and Alceste Scalas}, year = {2013}, title = {Choreography Synthesis as Contract Agreement}, booktitle = {ICE}, series = {{EPTCS}}, volume = {131}, pages = {52--67}, doi = {10.4204/EPTCS.131.6}, ) @inproceedings(Lopez:2015:PVM:2814270.2814302, author = {L\IeC{\'o}pez, Hugo A. and Eduardo R. B. Marques and Francisco Martins and Nicholas Ng and C\IeC{\'e}sar Santos and Vasco Thudichum Vasconcelos and Nobuko Yoshida}, year = {2015}, title = {Protocol-based Verification of Message-passing Parallel Programs}, booktitle = {OOPSLA}, publisher = {ACM}, pages = {280--298}, doi = {10.1145/2814270.2814302}, ) @inproceedings(DBLP:conf/pldi/RondonKJ08, author = {Patrick Maxim Rondon and Ming Kawaguchi and Ranjit Jhala}, year = {2008}, title = {Liquid Types}, booktitle = {POPL}, publisher = {{ACM}}, pages = {159--169}, doi = {10.1145/1375581.1375602}, ) @inbook(vasconcelos.etal:deductive-verification-of-mpi-protocols, author = {Vasco Thudichum Vasconcelos and Francisco Martins and Eduardo R. B. Marques and Nobuko Yoshida and Nicholas Ng}, year = {2017}, title = {Behavioural Types: From Theory to Practice}, chapter = {Deductive Verification of MPI Protocols}, publisher = {River Publishers}, ) @inproceedings(DBLP:conf/esop/VazouRJ13, author = {Niki Vazou and Patrick Maxim Rondon and Ranjit Jhala}, year = {2013}, title = {Abstract Refinement Types}, booktitle = {Programming Languages and Systems - 22nd European Symposium on Programming, {ESOP} 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2013, Rome, Italy, March 16-24, 2013. Proceedings}, series = {LNCS}, volume = {7792}, publisher = {Springer}, pages = {209--228}, doi = {10.1007/978-3-642-37036-6_13}, ) @inproceedings(xi.pfenning:dependent-types-practical-programming, author = {Hongwei Xi and Frank Pfenning}, year = {1999}, title = {Dependent Types in Practical Programming}, booktitle = {POPL}, publisher = {ACM}, pages = {214--227}, doi = {10.1145/292540.292560}, )