{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:46:39Z","timestamp":1750308399653,"version":"3.41.0"},"reference-count":84,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2022,12,21]],"date-time":"2022-12-21T00:00:00Z","timestamp":1671580800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Advanced Type Systems for Multicore Programming","award":["PTDC\/EIA-CCO\/122547"],"award-info":[{"award-number":["PTDC\/EIA-CCO\/122547"]}]},{"name":"LASIGE Research Unit","award":["UID\/CEC\/00408\/2019"],"award-info":[{"award-number":["UID\/CEC\/00408\/2019"]}]},{"name":"EC Cost Action EUTypes","award":["CA15123"],"award-info":[{"award-number":["CA15123"]}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EPSRC (EP\/T006544\/1, EP\/K011715\/1, EP\/K034413\/1, EP\/L00058X\/1, EP\/N027833\/1, EP\/N028201\/1, EP\/T006544\/1, EP\/T014709\/1, EP\/V000462\/1, and EP\/X015955\/1"],"award-info":[{"award-number":["EPSRC (EP\/T006544\/1, EP\/K011715\/1, EP\/K034413\/1, EP\/L00058X\/1, EP\/N027833\/1, EP\/N028201\/1, EP\/T006544\/1, EP\/T014709\/1, EP\/V000462\/1, and EP\/X015955\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"name":"NCSS\/EPSRC VeTSS","award":["7050-00034A"],"award-info":[{"award-number":["7050-00034A"]}]},{"name":"European Union Marie Sklodowska-Curie","award":["778233"],"award-info":[{"award-number":["778233"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2022,12,31]]},"abstract":"<jats:p>We present<jats:sc>ParTypes<\/jats:sc>, a type discipline for parallel programs. The model we have in mind comprises a fixed number of processes running in parallel and communicating via collective operations or point-to-point synchronous message exchanges. A type describes a protocol to be followed by each processes in a given program. We present the type theory, a core imperative programming language and its operational semantics, and prove that type checking is decidable (up to decidability of semantic entailment) and that well-typed programs do not deadlock and always terminate. The article is accompanied by a large number of examples drawn from the literature on parallel programming.<\/jats:p>","DOI":"10.1145\/3552519","type":"journal-article","created":{"date-parts":[[2022,8,10]],"date-time":"2022-08-10T12:16:56Z","timestamp":1660133816000},"page":"1-55","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A Type Discipline for Message Passing Parallel Programs"],"prefix":"10.1145","volume":"44","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9539-8861","authenticated-orcid":false,"given":"Vasco T.","family":"Vasconcelos","sequence":"first","affiliation":[{"name":"LASIGE, Faculdade de Ci\u00eancias, Universidade de Lisboa, PT"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8521-8273","authenticated-orcid":false,"given":"Francisco","family":"Martins","sequence":"additional","affiliation":[{"name":"LASIGE, Faculdade de Ci\u00eancias, Universidade de Lisboa, and University of the Azores, PT"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5162-7936","authenticated-orcid":false,"given":"Hugo-Andr\u00e9s","family":"L\u00f3pez","sequence":"additional","affiliation":[{"name":"University of Copenhagen and DCR Solutions A\/S, Copenhagen, DK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3925-8557","authenticated-orcid":false,"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[{"name":"Imperial College London, London, UK"}]}],"member":"320","published-online":{"date-parts":[[2022,12,21]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1007\/978-3-319-48989-6_7","volume-title":"FM 2016: Formal Methods, Lecture Notes in Computer Science (LNCS)","author":"B\u00f6hm Stanislav","year":"2016","unstructured":"Stanislav B\u00f6hm, Ond\u0159ej Meca, and Petr Jan\u010dar. 2016. State-space reduction of non-deterministically synchronizing systems applicable to deadlock detection in MPI. In FM 2016: Formal Methods, Lecture Notes in Computer Science (LNCS). Springer, 102\u2013118."},{"key":"e_1_3_2_3_2","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-3-319-52234-0_5","volume-title":"Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science (LNCS)","author":"Botbol Vincent","year":"2017","unstructured":"Vincent Botbol, Emmanuel Chailloux, and Tristan Le Gall. 2017. Static analysis of communicating processes using symbolic transducers. In Verification, Model Checking, and Abstract Interpretation, Lecture Notes in Computer Science (LNCS). Springer, 73\u201390."},{"key":"e_1_3_2_4_2","first-page":"571","volume-title":"CTS","author":"Bridges D.","year":"2009","unstructured":"D. Bridges and S. Mostashfi. 2009. Universal monitoring platform for interactive real-time expansive networks (UMPIRE). In CTS. IEEE, 571."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_9"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_32"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/2220365.2220367"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429101"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290342"},{"key":"e_1_3_2_10_2","series-title":"(LNCS)","first-page":"23","volume-title":"TPHOLs","author":"Cohen E.","year":"2009","unstructured":"E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. 2009. VCC: A practical system for verifying concurrent C. In TPHOLs, Lecture Notes in Computer Science (LNCS), Vol. 5674. Springer, 23\u201342."},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3332466.3374515"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(4:6)2012"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2833157.2833159"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500582"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/2643135.2643153"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3095075"},{"key":"e_1_3_2_17_2","first-page":"263","volume-title":"FM (LNCS)","author":"Forejt V.","year":"2014","unstructured":"V. Forejt, D. Kroening, G. Narayanswamy, and S. Sharma. 2014. Precise predictive analysis for discovering communication deadlocks in MPI programs. In FM (LNCS), Vol. 8442. Springer, 263\u2013278."},{"key":"e_1_3_2_18_2","volume-title":"MPI: A Message-Passing Interface Standard, Version 3.1","author":"Forum Message Passing Interface","year":"2015","unstructured":"Message Passing Interface Forum. 2015. MPI: A Message-Passing Interface Standard, Version 3.1. University of Tennessee."},{"key":"e_1_3_2_19_2","volume-title":"MPI: A Message-Passing Interface Standard, Version 4.0","author":"Forum Message Passing Interface","year":"2021","unstructured":"Message Passing Interface Forum. 2021. MPI: A Message-Passing Interface Standard, Version 4.0. University of Tennessee."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.5555\/527029"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290341"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2015.35"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.22"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2043174.2043194"},{"key":"e_1_3_2_27_2","first-page":"73","volume-title":"International Summer School Logics and Languages for Reliability and Security","author":"Gordon A. D.","year":"2010","unstructured":"A. D. Gordon and C. Fournet. 2010. Principles and applications of refinement types. In International Summer School Logics and Languages for Reliability and Security. IOS Press, 73\u2013104."},{"key":"e_1_3_2_28_2","volume-title":"Introduction to Parallel Computing","author":"Grama Ananth","year":"2003","unstructured":"Ananth Grama, Anshul Gupta, George Karpsis, and Vipin Kumar. 2003. Introduction to Parallel Computing. Addison Wesley."},{"key":"e_1_3_2_29_2","volume-title":"Using MPI: Portable Parallel Programming with the Message Passing Interface","author":"Gropp W.","year":"1999","unstructured":"W. Gropp, E. Lusk, and A. Skjellum. 1999. Using MPI: Portable Parallel Programming with the Message Passing Interface. MIT press."},{"key":"e_1_3_2_30_2","volume-title":"The N-Body Pipeline","author":"Hansen Per Brinch","year":"1991","unstructured":"Per Brinch Hansen. 1991. The N-Body Pipeline. Technical Report. Electrical Engineering and Computer Science Technical Reports Paper 120, College of Engineering and Computer Science, Syracuse University."},{"key":"e_1_3_2_31_2","first-page":"30:1\u201330:11","volume-title":"SC","author":"Hilbrich T.","year":"2012","unstructured":"T. Hilbrich, J. Protze, M. Schulz, B. R. de Supinski, and M. S. M\u00fcller. 2012. MPI runtime error detection with MUST: Advances in deadlock detection. In SC. IEEE\/ACM, 30:1\u201330:11."},{"key":"e_1_3_2_32_2","first-page":"53","volume-title":"Parallel Tools Workshop","author":"Hilbrich T.","year":"2009","unstructured":"T. Hilbrich, M. Schulz, B. R. de Supinski, and M. S. M\u00fcller. 2009. MUST: A scalable approach to runtime error detection in MPI programs. In Parallel Tools Workshop. Springer, 53\u201366."},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_3_2_35_2","first-page":"105","volume-title":"COB 2014, Lecture Notes in Computer Science, (LNCS)","author":"Honda Kohei","year":"2014","unstructured":"Kohei Honda, Raymond Hu, Rumyana Neykova, Tzu-Chun Chen, Romain Demangeon, Pierre-Malo Denielou, and Nobuko Yoshida. 2014. Structuring communication with session types. In COB 2014, Lecture Notes in Computer Science, (LNCS), vol. 8665. Springer, 105\u2013127."},{"key":"e_1_3_2_36_2","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/978-3-642-33518-1_37","volume-title":"Recent Advances in the Message Passing Interface, Lecture Notes in Computer Science (LNCS)","author":"Honda K.","year":"2012","unstructured":"K. Honda, E. R. B. Marques, F. Martins, N. Ng, V. T. Vasconcelos, and N. Yoshida. 2012. Verification of MPI programs using session types. In Recent Advances in the Message Passing Interface, Lecture Notes in Computer Science (LNCS), vol. 7490. Springer, 291\u2013293."},{"key":"e_1_3_2_37_2","first-page":"55","volume-title":"ICDCIT, Lecture Notes in Computer Science (LNCS)","author":"Honda K.","year":"2011","unstructured":"K. Honda, A. Mukhamedov, G. Brown, T. Chen, and N. Yoshida. 2011. Scribbling interactions with a formal foundation. In ICDCIT, Lecture Notes in Computer Science (LNCS), vol. 6536. Springer, 55\u201375."},{"key":"e_1_3_2_38_2","first-page":"122","volume-title":"ESOP, Lecture Notes in Computer Science (LNCS)","author":"Honda K.","year":"1998","unstructured":"K. Honda, V. T. Vasconcelos, and M. Kubo. 1998. Language primitives and type discipline for structured communication-based programming. In ESOP, Lecture Notes in Computer Science (LNCS), vol. 1381. Springer, 122\u2013138."},{"key":"e_1_3_2_39_2","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/1328438.1328472","volume-title":"POPL","author":"Honda K.","year":"2008","unstructured":"K. Honda, N. Yoshida, and M. Carbone. 2008. Multiparty asynchronous session types. In POPL. ACM, 273\u2013284."},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_3_2_41_2","first-page":"466","volume-title":"Formal Methods, Lecture Notes in Computer Science (LNCS)","author":"Khanna Dhriti","year":"2018","unstructured":"Dhriti Khanna, Subodh Sharma, C\u00e9sar Rodr\u00edguez, and Rahul Purandare. 2018. Dynamic symbolic verification of MPI programs. In Formal Methods, Lecture Notes in Computer Science (LNCS). Springer, 466\u2013484."},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.155.4"},{"key":"e_1_3_2_43_2","first-page":"61","volume-title":"Parallel Tools Workshop","author":"Krammer B.","year":"2008","unstructured":"B. Krammer, T. Hilbrich, V. Himmler, B. Czink, K. Dichev, and M. S. M\u00fcller. 2008. MPI correctness checking with marmot. In Parallel Tools Workshop. Springer, 61\u201378."},{"key":"e_1_3_2_44_2","volume-title":"Synthesis of correct-by-construction MPI programs","author":"Lemos F.","year":"2014","unstructured":"F. Lemos. 2014. Synthesis of correct-by-construction MPI programs. Master\u2019s Thesis. Department of Informatics, University of Lisbon."},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3019612.3019656"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-39570-8_13"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814302"},{"key":"e_1_3_2_48_2","first-page":"103","volume-title":"PLACES (EPTCS)","author":"Marques E. R. B.","year":"2013","unstructured":"E. R. B. Marques, F. Martins, V. T. Vasconcelos, N. Ng, and N. Martins. 2013. Towards deductive verification of MPI programs against session types. In PLACES (EPTCS), Vol. 137. 103\u2013113."},{"key":"e_1_3_2_49_2","volume-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f P.","year":"1984","unstructured":"P. Martin-L\u00f6f. 1984. Intuitionistic Type Theory. Bibliopolis-Napoli."},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.246.6"},{"key":"e_1_3_2_51_2","first-page":"56","volume-title":"NASA Formal Methods, Lecture Notes in Computer Science (LNCS)","author":"Moskal M.","year":"2011","unstructured":"M. Moskal. 2011. Verifying functional correctness of C programs with VCC. In NASA Formal Methods, Lecture Notes in Computer Science (LNCS), vol. 6617. Springer, 56\u201357."},{"key":"e_1_3_2_52_2","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/978-3-662-43376-8_8","volume-title":"Coordination Models and Languages","author":"Mostrous Dimitris","year":"2014","unstructured":"Dimitris Mostrous and Vasco Thudichum Vasconcelos. 2014. Affine sessions. In Coordination Models and Languages. Springer, Berlin, 115\u2013130."},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.2200\/S00962ED2V01Y201910CAC049"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46663-6_11"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11761-014-0172-8"},{"key":"e_1_3_2_56_2","first-page":"329","volume-title":"Behavioural Types: From Theory to Tools","author":"Ng Nicholas","year":"2017","unstructured":"Nicholas Ng and Nobuko Yoshida. 2017. Behavioural Types: From Theory to Tools. River Publishers, Chapter Protocol-Driven MPI Program Generation, 329\u2013352."},{"key":"e_1_3_2_57_2","series-title":"LNCS","first-page":"202","volume-title":"TOOLS Europe","author":"Ng N.","year":"2012","unstructured":"N. Ng, N. Yoshida, and K. Honda. 2012. Multiparty session C: Safe parallel programming with message optimisation. In TOOLS Europe, Lecture Notes in Computer Science (LNCS), vol. 7304. Springer, 202\u2013218."},{"key":"e_1_3_2_58_2","volume-title":"Parallel Programming with MPI","author":"Pacheco P. S.","year":"1997","unstructured":"P. S. Pacheco. 1997. Parallel Programming with MPI. Morgan Kaufmann."},{"key":"e_1_3_2_59_2","series-title":"LNCS","first-page":"344","volume-title":"PVM\/MPI","author":"Pervez S.","year":"2007","unstructured":"S. Pervez, G. Gopalakrishnan, R. M. Kirby, R. Palmer, R. Thakur, and W. Gropp. 2007. Practical model-checking method for verifying correctness of MPI programs. In PVM\/MPI, Lecture Notes in Computer Science, (LNCS), vol. 4757. Springer, 344\u2013353."},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04818-0"},{"key":"e_1_3_2_63_2","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/978-1-4612-4118-8_4","volume-title":"ALGOL-like Languages, Volume 1","author":"Reynolds John C.","year":"1997","unstructured":"John C. Reynolds. 1997. ALGOL-like Languages, Volume 1. Birkhauser Boston Inc., Chapter The Essence of ALGOL, 67\u201388. http:\/\/dl.acm.org\/citation.cfm?id=251167.251168."},{"key":"e_1_3_2_64_2","first-page":"159","volume-title":"PLDI","author":"Rondon P. M.","year":"2008","unstructured":"P. M. Rondon, M. Kawaguchi, and R. Jhala. 2008. Liquid types. In PLDI. ACM, 159\u2013169."},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.189"},{"key":"e_1_3_2_66_2","first-page":"193","volume-title":"ICPP","author":"Schulz M.","year":"2006","unstructured":"M. Schulz and B. R. de Supinski. 2006. A flexible and dynamic infrastructure for MPI tool interoperability. In ICPP. IEEE, 193\u2013202."},{"key":"e_1_3_2_67_2","unstructured":"Scribble 2015. Scribble Homepage. http:\/\/www.scribble.org\/. (2015)."},{"key":"e_1_3_2_68_2","first-page":"158","volume-title":"CEFP, Lecture Notes in Computer Science (LNCS)","author":"Sheard T.","year":"2007","unstructured":"T. Sheard and N. Linger. 2007. Programming in Omega. In CEFP, Lecture Notes in Computer Science (LNCS), vol. 5161. Springer, 158\u2013227."},{"key":"e_1_3_2_69_2","first-page":"2","volume-title":"VMCAI, Lecture Notes in Computer Science (LNCS)","author":"Siegel S. F.","year":"2011","unstructured":"S. F. Siegel and G. Gopalakrishnan. 2011. Formal analysis of message passing. In VMCAI, Lecture Notes in Computer Science (LNCS), vol. 6538. Springer, 2\u201318."},{"key":"e_1_3_2_70_2","first-page":"274","volume-title":"EuroPVM\/MPI, Lecture Notes in Computer Science (LNCS)","author":"Siegel S. F.","year":"2008","unstructured":"S. F. Siegel and L. F. Rossi. 2008. Analyzing BlobFlow: A case study using model checking to verify parallel scientific software. In EuroPVM\/MPI, Lecture Notes in Computer Science (LNCS), vol. 5205. Springer, 274\u2013282."},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1145\/2807591.2807635"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-011-0101-6"},{"key":"e_1_3_2_73_2","first-page":"412","volume-title":"VMCAI, Lecture Notes in Computer Science (LNCS)","author":"Siegel S. F.","year":"2012","unstructured":"S. F. Siegel and T. K. Zirkel. 2012. Loop invariant symbolic execution for parallel programs. In VMCAI, Lecture Notes in Computer Science (LNCS), vol. 7148. Springer, 412\u2013427."},{"key":"e_1_3_2_74_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.11.005"},{"key":"e_1_3_2_76_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_7"},{"key":"e_1_3_2_77_2","volume-title":"Liquid Haskell: Haskell as a Theorem Prover","author":"Vazou Niki","year":"2016","unstructured":"Niki Vazou. 2016. Liquid Haskell: Haskell as a Theorem Prover. Ph.D. Dissertation. University of California, San Diego, USA. http:\/\/www.escholarship.org\/uc\/item\/8dm057ws."},{"key":"e_1_3_2_78_2","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2010.7"},{"key":"e_1_3_2_79_2","unstructured":"W3C. 2004. W3C WS-CDL. http:\/\/www.w3.org\/2002\/ws\/chor\/. (2004)."},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","DOI":"10.1145\/3397495"},{"key":"e_1_3_2_81_2","first-page":"375","volume-title":"LICS","author":"Xi H.","year":"2000","unstructured":"H. Xi. 2000. Imperative programming with dependent types. In LICS. IEEE, 375\u2013387."},{"key":"e_1_3_2_82_2","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1145\/292540.292560","volume-title":"POPL","author":"Xi H.","year":"1999","unstructured":"H. Xi and F. Pfenning. 1999. Dependent types in practical programming. In POPL. ACM, 214\u2013227."},{"key":"e_1_3_2_83_2","first-page":"22","volume-title":"TGC (LNCS)","author":"Yoshida Nobuko","year":"2013","unstructured":"Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. 2013. The scribble protocol language. In TGC (LNCS), Vol. 8358. Springer, 22\u201341."},{"key":"e_1_3_2_84_2","doi-asserted-by":"publisher","DOI":"10.1145\/3183440.3190336"},{"key":"e_1_3_2_85_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428216"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3552519","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3552519","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:45:12Z","timestamp":1750268712000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3552519"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,21]]},"references-count":84,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,12,31]]}},"alternative-id":["10.1145\/3552519"],"URL":"https:\/\/doi.org\/10.1145\/3552519","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2022,12,21]]},"assertion":[{"value":"2020-05-20","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-07-05","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-12-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}