{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:02:13Z","timestamp":1767927733728,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,9,24]],"date-time":"2013-09-24T00:00:00Z","timestamp":1379980800000},"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":[[2013,9,24]]},"DOI":"10.1145\/2502409.2502411","type":"proceedings-article","created":{"date-parts":[[2013,9,17]],"date-time":"2013-09-17T19:57:05Z","timestamp":1379447825000},"page":"13-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["New equations for neutral terms"],"prefix":"10.1145","author":[{"given":"Guillaume","family":"Allais","sequence":"first","affiliation":[{"name":"University of Strathclyde, Glasgow, United Kingdom"}]},{"given":"Conor","family":"McBride","sequence":"additional","affiliation":[{"name":"University of Strathclyde, Glasgow, United Kingdom"}]},{"given":"Pierre","family":"Boutillier","sequence":"additional","affiliation":[{"name":"Paris Diderot, Paris, France"}]}],"member":"320","published-online":{"date-parts":[[2013,9,24]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007266"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.025"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.33"},{"key":"e_1_3_2_1_4_1","volume-title":"University of Cambridge","author":"Ahman D.","year":"2012"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.09.007"},{"key":"e_1_3_2_1_6_1","volume-title":"University of Strathclyde, 2012","author":"Allais G.","year":"2012"},{"key":"e_1_3_2_1_7_1","volume-title":"Slides","author":"Allais G.","year":"2013"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/647849.737066"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_3_2_1_10_1","unstructured":"R. Atkey. A type checker that knows its monad from its elbow. Blog post December 2011. URL http:\/\/bentnib.org\/posts\/2011-12-14-type-checker.html.  R. Atkey. A type checker that knows its monad from its elbow. Blog post December 2011. URL http:\/\/bentnib.org\/posts\/2011-12-14-type-checker.html."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11753728_7"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54487-9"},{"key":"e_1_3_2_1_13_1","volume-title":"ENS Lyon","author":"Boutillier P.","year":"2009"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/321864.321875"},{"key":"e_1_3_2_1_15_1","unstructured":"J.\n       \n      Chapman T.\n       \n      Altenkirch and \n      \n      \n      C.\n       \n      McBride\n    .\n      \n  \n   \n  Epigram reloaded: a standalone typechecker for ETT. In M. C. J. D. van Eekelen editor Trends in Functional Programming volume \n  6\n   of \n  Trends in Functional Programming pages \n  79\n  --\n  94\n  . \n  Intellect 2005\n  .  J. Chapman T. Altenkirch and C. McBride. Epigram reloaded: a standalone typechecker for ETT. In M. C. J. D. van Eekelen editor Trends in Functional Programming volume 6 of Trends in Functional Programming pages 79--94. Intellect 2005."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1932681.1863547"},{"key":"e_1_3_2_1_17_1","volume-title":"University of Nottingham","author":"Chapman J. M.","year":"2009"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019964114625"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129596002150"},{"key":"e_1_3_2_1_20_1","unstructured":"P.-E. Dagand and C. McBride. Elaborating Inductive Definitions. ArXiv e-prints Oct. 2012.  P.-E. Dagand and C. McBride. Elaborating Inductive Definitions. ArXiv e-prints Oct. 2012."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"N. A.\n       \n      Danielsson\n    .\n      \n  \n   \n  A formalisation of a dependently typed language as an Inductive-Recursive family. In T. Altenkirch and C. McBride editors Types for Proofs and Programs volume \n  4502\n   of \n  Lecture Notes in Computer Science pages \n  93\n  --\n  109\n  . \n  Springer 2007\n  .   N. A. Danielsson. A formalisation of a dependently typed language as an Inductive-Recursive family. In T. Altenkirch and C. McBride editors Types for Proofs and Programs volume 4502 of Lecture Notes in Computer Science pages 93--109. Springer 2007.","DOI":"10.1007\/978-3-540-74464-1_7"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"O.\n       \n      Danvy\n    .\n      \n  \n   \n  Type-directed partial evaluation. In J. Hatcliff T. Mogensen and P. Thiemann editors Partial Evaluation volume \n  1706\n   of \n  Lecture Notes in Computer Science chapter 16 pages \n  367\n  --\n  411\n  . \n  Springer Berlin Heidelberg 1999\n  .   O. Danvy. Type-directed partial evaluation. In J. Hatcliff T. Mogensen and P. Thiemann editors Partial Evaluation volume 1706 of Lecture Notes in Computer Science chapter 16 pages 367--411. Springer Berlin Heidelberg 1999.","DOI":"10.1007\/3-540-47018-2_16"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_1_24_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/3-540-48959-2_11","volume-title":"J.-Y","author":"Dybjer P.","year":"1999"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"A.\n       \n      Filinski\n    .\n      \n  \n   \n  Normalization by evaluation for the computational Lambda-Calculus. In S. Abramsky editor Typed Lambda Calculi and Applications volume \n  2044\n   of \n  Lecture Notes in Computer Science chapter 15 pages \n  151\n  --\n  165\n  . \n  Springer Apr. \n  2001\n  .   A. Filinski. Normalization by evaluation for the computational Lambda-Calculus. In S. Abramsky editor Typed Lambda Calculi and Applications volume 2044 of Lecture Notes in Computer Science chapter 15 pages 151--165. Springer Apr. 2001.","DOI":"10.1007\/3-540-45413-6_15"},{"key":"e_1_3_2_1_26_1","volume-title":"Hermann","author":"Girard J.","year":"2006"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/583852.581501"},{"key":"e_1_3_2_1_28_1","unstructured":"INRIA. The Coq proof assistant.  INRIA. The Coq proof assistant."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863597.1863601"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/604174.604179"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508006956"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863495.1863497"},{"key":"e_1_3_2_1_33_1","unstructured":"C. McBride. EE-PigWeek 4--9 Jan 2010. Blog post January 2010. URL http:\/\/www.e-pig.org\/epilogue\/?p=306.  C. McBride. EE-PigWeek 4--9 Jan 2010. Blog post January 2010. URL http:\/\/www.e-pig.org\/epilogue\/?p=306."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"crossref","unstructured":"U.\n       \n      Norell\n    .\n      \n  \n   \n  Dependently typed programming in Agda. In P. W. M. Koopman R. Plasmeijer and S. D. Swierstra editors Advanced Functional Programming volume \n  5832\n   of \n  Lecture Notes in Computer Science pages \n  230\n  --\n  266\n  . \n  Springer 2008\n  .   U. Norell. Dependently typed programming in Agda. In P. W. M. Koopman R. Plasmeijer and S. D. Swierstra editors Advanced Functional Programming volume 5832 of Lecture Notes in Computer Science pages 230--266. Springer 2008.","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"e_1_3_2_1_36_1","volume-title":"UNC","author":"Pagano M. M.","year":"2012"},{"key":"e_1_3_2_1_37_1","volume-title":"Twenty Five Years of Constructive Type Theory","author":"Palmgren E.","year":"1998"},{"key":"e_1_3_2_1_38_1","volume-title":"University of Edinburgh","author":"Pollack R.","year":"1994"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004641"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"crossref","unstructured":"K.\n       \n      Watkins I.\n       \n      Cervesato F.\n       \n      Pfenning and \n      \n      \n      D.\n       \n      Walker\n      \n  \n  . \n  A concurrent logical framework: The propositional fragment. In S. Berardi M. Coppo and F. Damiani editors TYPES volume \n  3085\n   of \n  Lecture Notes in Computer Science pages \n  355\n  --\n  377\n  . \n  Springer 2003\n  .  K. Watkins I. Cervesato F. Pfenning and D. Walker. A concurrent logical framework: The propositional fragment. In S. Berardi M. Coppo and F. Damiani editors TYPES volume 3085 of Lecture Notes in Computer Science pages 355--377. Springer 2003.","DOI":"10.1007\/978-3-540-24849-1_23"}],"event":{"name":"ICFP'13: ACM SIGPLAN International Conference on Functional Programming","location":"Boston Massachusetts USA","acronym":"ICFP'13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2502409.2502411","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2502409.2502411","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:35Z","timestamp":1750231715000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2502409.2502411"}},"subtitle":["a sound and complete decision procedure, formalized"],"short-title":[],"issued":{"date-parts":[[2013,9,24]]},"references-count":40,"alternative-id":["10.1145\/2502409.2502411","10.1145\/2502409"],"URL":"https:\/\/doi.org\/10.1145\/2502409.2502411","relation":{},"subject":[],"published":{"date-parts":[[2013,9,24]]},"assertion":[{"value":"2013-09-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}