{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:28:59Z","timestamp":1784255339903,"version":"3.55.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ERC","award":["64399"],"award-info":[{"award-number":["64399"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,7,26]]},"abstract":"<jats:p>Equations is a plugin for the Coq proof assistant which provides a notation for defining programs by dependent pattern-matching and structural or well-founded recursion. It additionally derives useful high-level proof principles for demonstrating properties about them, abstracting away from the implementation details of the function and its compiled form. We present a general design and implementation that provides a robust and expressive function definition package as a definitional extension to the Coq kernel. At the core of the system is a new simplifier for dependent equalities based on an original handling of the no-confusion property of constructors.<\/jats:p>","DOI":"10.1145\/3341690","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["Equations reloaded: high-level dependently-typed functional programming and proving in Coq"],"prefix":"10.1145","volume":"3","author":[{"given":"Matthieu","family":"Sozeau","sequence":"first","affiliation":[{"name":"Inria, France \/ IRIF, France \/ University of Paris Diderot, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cyprien","family":"Mangin","sequence":"additional","affiliation":[{"name":"Inria, France \/ IRIF, France \/ University of Paris Diderot, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_5"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000022"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110277"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292608"},{"key":"e_1_2_2_5_1","volume-title":"Matthieu Sozeau, and Matthew Weaver.","author":"Anand Abhishek","year":"2017"},{"key":"e_1_2_2_6_1","unstructured":"Jeremy Avigad Gabriel Ebner and Sebastian Ullrich. 2017. The Lean Reference Manual release 3.3.0. Available at https:\/\/leanprover.github.io\/reference\/lean_reference.pdf .  Jeremy Avigad Gabriel Ebner and Sebastian Ullrich. 2017. The Lean Reference Manual release 3.3.0. Available at https:\/\/leanprover.github.io\/reference\/lean_reference.pdf ."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_9"},{"key":"e_1_2_2_8_1","volume-title":"TYPES (Lecture Notes in Computer Science)","author":"Brady Edwin"},{"key":"e_1_2_2_9_1","doi-asserted-by":"crossref","volume-title":"Certified Programming with Dependent Types","author":"Chlipala Adam","DOI":"10.7551\/mitpress\/9153.001.0001"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236770"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018612"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681800014X"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628139"},{"key":"e_1_2_2_15_1","unstructured":"Thierry Coquand. 1992. Pattern Matching with Dependent Types. http:\/\/www.cs.chalmers.se\/~coquand\/pattern.ps Proceedings of the Workshop on Logical Frameworks.  Thierry Coquand. 1992. Pattern Matching with Dependent Types. http:\/\/www.cs.chalmers.se\/~coquand\/pattern.ps Proceedings of the Workshop on Logical Frameworks."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_2_2_17_1","volume-title":"Essays Dedicated to Joseph A. Goguen (Lecture Notes in Computer Science), Kokichi Futatsugi, Jean-Pierre Jouannaud, and Jos\u00e9 Meseguer (Eds.)","author":"Goguen Healfdene"},{"key":"e_1_2_2_19_1","doi-asserted-by":"crossref","volume-title":"A Groupoid Model Refutes Uniqueness of Identity Proofs","author":"Hofmann Martin","DOI":"10.1109\/LICS.1994.316071"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_2_2_21_1","series-title":"Lecture Notes in Computer Science","volume-title":"Generalizations of Hedberg\u2019s Theorem","author":"Kraus Nicolai"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_48"},{"key":"e_1_2_2_23_1","volume-title":"Weak omega-categories from intensional type theory. Logical Methods in Computer Science 6, 3","author":"LeFanu Lumsdaine Peter","year":"2010"},{"key":"e_1_2_2_24_1","unstructured":"Assia Mahboubi Enrico Tassi Yves Bertot and Georges Gonthier. 2018. Mathematical Components.  Assia Mahboubi Enrico Tassi Yves Bertot and Georges Gonthier. 2018. Mathematical Components."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.185.5"},{"key":"e_1_2_2_26_1","volume-title":"Studies in Proof Theory","volume":"1","author":"Martin-L\u00f6f Per","year":"1984"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_12"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_2_2_30_1","volume-title":"Handcrafted Inversions Made Operational on Operational Semantics","author":"Monin Jean-Fran\u00e7ois"},{"key":"e_1_2_2_32_1","unstructured":"Christine Paulin-Mohring. 1996. D\u00e9finitions Inductives en Th\u00e9orie des Types d\u2019Ordre Sup\u00e9rieur. Habilitation \u00e0 diriger les recherches. Universit\u00e9 Claude Bernard Lyon I. http:\/\/www.lri.fr\/~paulin\/PUBLIS\/habilitation.ps.gz  Christine Paulin-Mohring. 1996. D\u00e9finitions Inductives en Th\u00e9orie des Types d\u2019Ordre Sup\u00e9rieur. Habilitation \u00e0 diriger les recherches. Universit\u00e9 Claude Bernard Lyon I. http:\/\/www.lri.fr\/~paulin\/PUBLIS\/habilitation.ps.gz"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(86)80002-5"},{"key":"e_1_2_2_34_1","volume-title":"ESOP 2018 - 27th European Symposium on Programming (LNCS)","volume":"10801","author":"P\u00e9drot Pierre-Marie","year":"2018"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158104"},{"key":"e_1_2_2_36_1","unstructured":"Daniel Schepler. 2013. Bijective function implies equal types is provably inconsistent with functional extensionality in Coq. Post on coq-club. https:\/\/sympa.inria.fr\/sympa\/arc\/coq-club\/2013-12\/msg00114.html  Daniel Schepler. 2013. Bijective function implies equal types is provably inconsistent with functional extensionality in Coq. Post on coq-club. https:\/\/sympa.inria.fr\/sympa\/arc\/coq-club\/2013-12\/msg00114.html"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291156"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_29"},{"key":"e_1_2_2_39_1","doi-asserted-by":"crossref","unstructured":"Matthieu Sozeau and Cyprien Mangin. 2019a. Equations Reloaded Accompanying Material. Available on the ACM DL.  Matthieu Sozeau and Cyprien Mangin. 2019a. Equations Reloaded Accompanying Material. Available on the ACM DL.","DOI":"10.1145\/3342526"},{"key":"e_1_2_2_40_1","doi-asserted-by":"crossref","unstructured":"Matthieu Sozeau and Cyprien Mangin. 2019b. Equations v1.2.  Matthieu Sozeau and Cyprien Mangin. 2019b. Equations v1.2.","DOI":"10.1145\/3341690"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167092"},{"key":"e_1_2_2_42_1","unstructured":"Thomas Streicher. 1993. Semantical Investigations into Intensional Type Theory. Habilitationsschrift. LMU M\u00fcnchen.  Thomas Streicher. 1993. Semantical Investigations into Intensional Type Theory. Habilitationsschrift. LMU M\u00fcnchen."},{"key":"e_1_2_2_43_1","volume-title":"Homotopy Type Theory: Univalent Foundations for Mathematics","author":"Foundations Program The Univalent"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122963"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_17"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341690","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341690","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:30Z","timestamp":1750200090000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341690"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":42,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341690"],"URL":"https:\/\/doi.org\/10.1145\/3341690","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}