{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:12:43Z","timestamp":1750306363102,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":52,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,9,18]],"date-time":"2016-09-18T00:00:00Z","timestamp":1474156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000921","name":"European Cooperation in Science and Technology","doi-asserted-by":"publisher","award":["EUTYPES"],"award-info":[{"award-number":["EUTYPES"]}],"id":[{"id":"10.13039\/501100000921","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["PIRSES-GA-2013-612638"],"award-info":[{"award-number":["PIRSES-GA-2013-612638"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,9,18]]},"DOI":"10.1145\/2976022.2976032","type":"proceedings-article","created":{"date-parts":[[2016,8,26]],"date-time":"2016-08-26T12:40:09Z","timestamp":1472215209000},"page":"28-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Programming with monadic CSP-style processes in dependent type theory"],"prefix":"10.1145","author":[{"given":"Bashar","family":"Igried","sequence":"first","affiliation":[{"name":"Swansea University, UK"}]},{"given":"Anton","family":"Setzer","sequence":"additional","affiliation":[{"name":"Swansea University, UK"}]}],"member":"320","published-online":{"date-parts":[[2016,9,18]]},"reference":[{"volume-title":"Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen","year":"2006","author":"Abel A.","key":"e_1_3_2_2_2_1"},{"first-page":"10","volume-title":"Coalgebraic Methods in Computer Science","author":"Abel A.","key":"e_1_3_2_2_3_1"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500591"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429075"},{"volume-title":"Functional Programming","year":"2016","author":"Abel A.","key":"e_1_3_2_2_6_1"},{"key":"e_1_3_2_2_7_1","unstructured":"Agda Community. The Agda Wiki. 2015.  Agda Community. The Agda Wiki. 2015."},{"volume-title":"Addison-Wesley","year":"2001","author":"Alexandrescu A.","key":"e_1_3_2_2_8_1"},{"key":"e_1_3_2_2_9_1","first-page":"1","volume-title":"Handbook of Dynamic System Modeling","author":"Baeten J.","year":"2007"},{"key":"e_1_3_2_2_10_1","unstructured":"J. A. Bergstra and J. W. Klop. Fixed point semantics in process algebras. CWI technical report Stichting Mathematisch Centrum. Informatica-IW 206\/82 1982.  J. A. Bergstra and J. W. Klop. Fixed point semantics in process algebras. CWI technical report Stichting Mathematisch Centrum. Informatica-IW 206\/82 1982."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80025-X"},{"first-page":"99","volume-title":"Language Engineering and Rigorous Software Development","author":"Bove A.","key":"e_1_3_2_2_12_1"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"e_1_3_2_2_14_1","unstructured":"E. Brady. Idris a language with dependent types \u2013 Extended abstract. 2008.  E. Brady. Idris a language with dependent types \u2013 Extended abstract. 2008."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/828.833"},{"key":"e_1_3_2_2_17_1","first-page":"83","volume-title":"CPA 2008","author":"Brown N. C. C.","year":"2008"},{"key":"e_1_3_2_2_18_1","first-page":"23","article-title":"Automatically generating CSP models for communicating Haskell processes","author":"Brown N. C. C.","year":"2009","journal-title":"ECEASST"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383954"},{"key":"e_1_3_2_2_20_1","unstructured":"Coq Community. The Coq Proof Assistant. 2015.  Coq Community. The Coq Proof Assistant. 2015."},{"key":"e_1_3_2_2_21_1","unstructured":"Coq Development Team. The Coq proof assistant. Reference manual. https:\/\/coq.inria.fr\/distrib\/current\/refman\/ 2015.  Coq Development Team. The Coq proof assistant. Reference manual. https:\/\/coq.inria.fr\/distrib\/current\/refman\/ 2015."},{"first-page":"78","volume-title":"Types for Proofs and Programs","author":"Coquand T.","key":"e_1_3_2_2_22_1"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/120477.120487"},{"volume-title":"Proceedings of the 1992 workshop on types for proofs and programs","year":"1992","author":"Dybjer P.","key":"e_1_3_2_2_24_1"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586554"},{"issue":"1","key":"e_1_3_2_2_26_1","first-page":"47","article-title":"Induction-recursion and initial algebras","volume":"124","author":"Dybjer P.","year":"2003","journal-title":"Annals of Pure and Applied Logic"},{"volume-title":"University of St Andrews","year":"2015","author":"Elliott A. S.","key":"e_1_3_2_2_27_1"},{"key":"e_1_3_2_2_28_1","unstructured":"ERTMS. The European Rail Traffic Mangement System. 2013.  ERTMS. The European Rail Traffic Mangement System. 2013."},{"volume-title":"Universit\u00e4tsund Landesbibliothek der Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf","year":"2011","author":"Fontaine M.","key":"e_1_3_2_2_29_1"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2013.08.012"},{"key":"e_1_3_2_2_31_1","unstructured":"S. Goncharov L. Schr\u00f6der and C. Rauch. (Co-)algebraic foundations for effect handling and iteration. CoRR abs\/1405.0854 2014.  S. Goncharov L. Schr\u00f6der and C. Rauch. (Co-)algebraic foundations for effect handling and iteration. CoRR abs\/1405.0854 2014."},{"volume-title":"Electronic proceedings of the workshop on dependent types in programming","year":"1999","author":"Hancock P.","key":"e_1_3_2_2_32_1"},{"key":"e_1_3_2_2_33_1","first-page":"317","volume-title":"LNCS","volume":"1862","author":"Hancock P.","year":"2000"},{"volume-title":"Workshop on subtyping and dependent types in programming, Portugal,7","year":"2000","author":"Hancock P.","key":"e_1_3_2_2_34_1"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"crossref","unstructured":"doi: 10.1145\/359576.359585.  doi: 10.1145\/359576.359585.","DOI":"10.1145\/359576.359585"},{"key":"e_1_3_2_2_37_1","unstructured":"B. Igried and A. Setzer. CSP-Agda. Agda library 2016.  B. Igried and A. Setzer. CSP-Agda. Agda library 2016."},{"volume-title":"Swansea University","year":"2012","author":"Kanso K.","key":"e_1_3_2_2_38_1"},{"first-page":"48","volume-title":"Proceedings of IFM \u201902","author":"L\u00f3pez N.","key":"e_1_3_2_2_39_1"},{"key":"e_1_3_2_2_40_1","unstructured":"ISBN 3-540-43703-7.  ISBN 3-540-43703-7."},{"key":"e_1_3_2_2_41_1","first-page":"105","volume-title":"Bibliopolis","author":"Martin-L\u00f6f P.","year":"1984"},{"volume-title":"Springer","year":"1982","author":"Milner R.","key":"e_1_3_2_2_42_1"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2005.09.006"},{"volume-title":"Chalmers University of Technology","year":"2007","author":"Norell U.","key":"e_1_3_2_2_45_1"},{"first-page":"95","volume-title":"Tools for Practical Software Verification: LASER","author":"Paulin-Mohring C.","key":"e_1_3_2_2_46_1"},{"volume-title":"Prentice Hall","year":"1997","author":"Roscoe A. W.","key":"e_1_3_2_2_47_1"},{"key":"e_1_3_2_2_48_1","unstructured":"S. Schneider. Concurrent and Real Time Systems: The CSP Approach. John Wiley 1st edition 1999. ISBN 0471623733.   S. Schneider. Concurrent and Real Time Systems: The CSP Approach. John Wiley 1st edition 1999. ISBN 0471623733."},{"first-page":"339","volume-title":"Proceedings of the International Workshop on Semantics of Specification Languages (SoSL)","author":"Sellink M. P. A.","key":"e_1_3_2_2_49_1"},{"key":"e_1_3_2_2_50_1","unstructured":"ISBN 3-540-19854-7.  ISBN 3-540-19854-7."},{"volume-title":"Conference Proceedings of TFP 2006, 2006. Available from http:\/\/www.cs.nott.ac.uk\/\u223cnhn\/TFP2006\/ TFP2006-Programme.html and http:\/\/www.cs.swan.ac.uk\/\u223ccsetzer\/index.html.","author":"Setzer A.","key":"e_1_3_2_2_51_1"},{"key":"e_1_3_2_2_52_1","first-page":"45","volume-title":"Rewriting and Typed Lambda Calculi","volume":"8560","author":"Setzer A."},{"key":"e_1_3_2_2_53_1","first-page":"370","volume-title":"CPA","volume":"65","author":"Welch P. H.","year":"2007"}],"event":{"name":"ICFP'16: ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Nara Japan","acronym":"ICFP'16"},"container-title":["Proceedings of the 1st International Workshop on Type-Driven Development"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2976022.2976032","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2976022.2976032","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:56:16Z","timestamp":1750222576000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2976022.2976032"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,18]]},"references-count":52,"alternative-id":["10.1145\/2976022.2976032","10.1145\/2976022"],"URL":"https:\/\/doi.org\/10.1145\/2976022.2976032","relation":{},"subject":[],"published":{"date-parts":[[2016,9,18]]},"assertion":[{"value":"2016-09-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}