{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:05Z","timestamp":1750221305544,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":22,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,8]],"date-time":"2018-01-08T00:00:00Z","timestamp":1515369600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,1,8]]},"DOI":"10.1145\/3167083","type":"proceedings-article","created":{"date-parts":[[2018,3,16]],"date-time":"2018-03-16T16:10:56Z","timestamp":1521216656000},"page":"252-265","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["HO\u03c0 in Coq"],"prefix":"10.1145","author":[{"given":"Sergue\u00ef","family":"Lenglet","sequence":"first","affiliation":[{"name":"University of Lorraine, France"}]},{"given":"Alan","family":"Schmitt","sequence":"additional","affiliation":[{"name":"Inria, France"}]}],"member":"320","published-online":{"date-parts":[[2018,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Crole","author":"Ambler Simon","year":"1999","unstructured":"Simon Ambler and Roy L . Crole . 1999 . Mechanized Operational Semantics via (Co)Induction. In TPHOLs\u201999 (Lecture Notes in Computer Science), Yves Bertot, Gilles Dowek, Andr\u00e9 Hirschowitz, Christine Paulin-Mohring, and Laurent Th\u00e9ry (Eds.), Vol. 1690 . Springer , Nice, France, 221\u2013238. Simon Ambler and Roy L. Crole. 1999. Mechanized Operational Semantics via (Co)Induction. In TPHOLs\u201999 (Lecture Notes in Computer Science), Yves Bertot, Gilles Dowek, Andr\u00e9 Hirschowitz, Christine Paulin-Mohring, and Laurent Th\u00e9ry (Eds.), Vol. 1690. Springer, Nice, France, 221\u2013238."},{"volume-title":"ITP 2014 (Lecture Notes in Computer Science)","author":"Anand Abhishek","key":"e_1_3_2_1_2_1","unstructured":"Abhishek Anand and Vincent Rahli . 2014. Towards a Formally Verified Proof Assistant . In ITP 2014 (Lecture Notes in Computer Science) , Gerwin Klein and Ruben Gamboa (Eds.), Vol. 8558 . Springer , Vienna, Austria , 27\u201344. Abhishek Anand and Vincent Rahli. 2014. Towards a Formally Verified Proof Assistant. In ITP 2014 (Lecture Notes in Computer Science), Gerwin Klein and Ruben Gamboa (Eds.), Vol. 8558. Springer, Vienna, Austria, 27\u201344."},{"key":"e_1_3_2_1_3_1","first-page":"1","article-title":"Abella: A System for Reasoning about Relational Specifications","volume":"7","author":"Baelde David","year":"2014","unstructured":"David Baelde , Kaustuv Chaudhuri , Andrew Gacek , Dale Miller , Gopalan Nadathur , Alwen Tiu , and Yuting Wang . 2014 . Abella: A System for Reasoning about Relational Specifications . J. Formalized Reasoning 7 , 2 (2014), 1 \u2013 89 . David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. 2014. Abella: A System for Reasoning about Relational Specifications. J. Formalized Reasoning 7, 2 (2014), 1\u201389.","journal-title":"J. Formalized Reasoning"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003366"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"e_1_3_2_1_6_1","volume-title":"TLC: A non-constructive library for Coq.","author":"Chargu\u00e9raud Arthur","year":"2017","unstructured":"Arthur Chargu\u00e9raud . 2017 . TLC: A non-constructive library for Coq. (2017). http:\/\/www.chargueraud.org\/softs\/tlc\/ Arthur Chargu\u00e9raud. 2017. TLC: A non-constructive library for Coq. (2017). http:\/\/www.chargueraud.org\/softs\/tlc\/"},{"volume-title":"MOVEP\u20192K \u2013 4th Summer school on Modelling and Verification of Parallel processes (Lecture Notes in Computer Science)","author":"Zilio Silvano Dal","key":"e_1_3_2_1_7_1","unstructured":"Silvano Dal Zilio . 2001. Mobile Processes: a Commented Bibliography . In MOVEP\u20192K \u2013 4th Summer school on Modelling and Verification of Parallel processes (Lecture Notes in Computer Science) , Vol. 2067 . Springer-Verlag , 206\u2013222. Silvano Dal Zilio. 2001. Mobile Processes: a Commented Bibliography. In MOVEP\u20192K \u2013 4th Summer school on Modelling and Verification of Parallel processes (Lecture Notes in Computer Science), Vol. 2067. Springer-Verlag, 206\u2013222."},{"key":"e_1_3_2_1_8_1","unstructured":"Edkso de Vries and Vasileios Koutavas. 2012. Locally Nameless Permutation Types. (2012). available at http:\/\/edsko.net\/pubs\/lnpt.pdf .  Edkso de Vries and Vasileios Koutavas. 2012. Locally Nameless Permutation Types. (2012). available at http:\/\/edsko.net\/pubs\/lnpt.pdf ."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/646528.695050"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80013-6"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0008"},{"key":"e_1_3_2_1_12_1","volume-title":"Howe\u2019s Method for Contextual Semantics. In 26th International Conference on Concurrency Theory, CONCUR 2015 (LIPIcs), Luca Aceto and David de Frutos-Escrig (Eds.)","volume":"42","author":"Lenglet Sergue\u00ef","year":"2015","unstructured":"Sergue\u00ef Lenglet and Alan Schmitt . 2015 . Howe\u2019s Method for Contextual Semantics. In 26th International Conference on Concurrency Theory, CONCUR 2015 (LIPIcs), Luca Aceto and David de Frutos-Escrig (Eds.) , Vol. 42 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Madrid, Spain, 212\u2013225. Sergue\u00ef Lenglet and Alan Schmitt. 2015. Howe\u2019s Method for Contextual Semantics. In 26th International Conference on Concurrency Theory, CONCUR 2015 (LIPIcs), Luca Aceto and David de Frutos-Escrig (Eds.), Vol. 42. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Madrid, Spain, 212\u2013225."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.08.002"},{"volume-title":"ITP 2015 (Lecture Notes in Computer Science)","author":"Maksimovic Petar","key":"e_1_3_2_1_14_1","unstructured":"Petar Maksimovic and Alan Schmitt . 2015. HOCore in Coq . In ITP 2015 (Lecture Notes in Computer Science) , Christian Urban and Xingyuan Zhang (Eds.), Vol. 9236 . Springer , Nanjing, China , 278\u2013293. Petar Maksimovic and Alan Schmitt. 2015. HOCore in Coq. In ITP 2015 (Lecture Notes in Computer Science), Christian Urban and Xingyuan Zhang (Eds.), Vol. 9236. Springer, Nanjing, China, 278\u2013293."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364406.2364411"},{"key":"e_1_3_2_1_16_1","volume-title":"Higher-order psi-calculi. Mathematical Structures in Computer Science FirstView (3","author":"Parrow Joachim","year":"2014","unstructured":"Joachim Parrow , Johannes Borgstr\u00f6m , Palle Raabjerg , and Johannes \u00c5man Pohjola . 2014. Higher-order psi-calculi. Mathematical Structures in Computer Science FirstView (3 2014 ), 1\u201337. Joachim Parrow, Johannes Borgstr\u00f6m, Palle Raabjerg, and Johannes \u00c5man Pohjola. 2014. Higher-order psi-calculi. Mathematical Structures in Computer Science FirstView (3 2014), 1\u201337."},{"key":"e_1_3_2_1_17_1","unstructured":"Roly Perera and James Cheney. 2016. Proof-relevant \u03c0 -calculus: a constructive account of concurrency and causality. (2016). arXiv: cs.LO\/1604.04575v2  Roly Perera and James Cheney. 2016. Proof-relevant \u03c0 -calculus: a constructive account of concurrency and causality. (2016). arXiv: cs.LO\/1604.04575v2"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0096"},{"volume-title":"The Pi-Calculus: A Theory of Mobile Processes","author":"Sangiorgi Davide","key":"e_1_3_2_1_21_1","unstructured":"Davide Sangiorgi and David Walker . 2001. The Pi-Calculus: A Theory of Mobile Processes . Cambridge University Press . Davide Sangiorgi and David Walker. 2001. The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press."},{"key":"e_1_3_2_1_22_1","unstructured":"David Thibodeau Alberto Momigliano and Brigitte Pientka. 2016. A Case-Study in Programming Coinductive Proofs: Howe\u2019s Method. (2016). available at momigliano.di.unimi.it\/papers\/bhowe.pdf .  David Thibodeau Alberto Momigliano and Brigitte Pientka. 2016. A Case-Study in Programming Coinductive Proofs: Howe\u2019s Method. (2016). available at momigliano.di.unimi.it\/papers\/bhowe.pdf ."}],"event":{"name":"CPP '18: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Los Angeles CA USA","acronym":"CPP '18"},"container-title":["Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167083","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3167083","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:27Z","timestamp":1750212807000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167083"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,8]]},"references-count":22,"alternative-id":["10.1145\/3167083","10.1145\/3176245"],"URL":"https:\/\/doi.org\/10.1145\/3167083","relation":{},"subject":[],"published":{"date-parts":[[2018,1,8]]},"assertion":[{"value":"2018-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}