{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:11:14Z","timestamp":1763467874675,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2008,7,15]],"date-time":"2008-07-15T00:00:00Z","timestamp":1216080000000},"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":[[2008,7,15]]},"DOI":"10.1145\/1389449.1389456","type":"proceedings-article","created":{"date-parts":[[2008,7,22]],"date-time":"2008-07-22T13:46:39Z","timestamp":1216734399000},"page":"44-55","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["'Galculator'"],"prefix":"10.1145","author":[{"given":"Paulo F.","family":"Silva","sequence":"first","affiliation":[{"name":"University of Minho, Braga, Portugal"}]},{"given":"Jos\u00e9 N.","family":"Oliveira","sequence":"additional","affiliation":[{"name":"University of Minho, Braga, Portugal"}]}],"member":"320","published-online":{"date-parts":[[2008,7,15]]},"reference":[{"volume-title":"December","year":"1992","author":"Aarts C.","key":"e_1_3_2_1_1_1"},{"volume-title":"Program verification in Coq","year":"2008","author":"Almeida J.C.","key":"e_1_3_2_1_2_1"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581494"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2003.06.002"},{"volume-title":"Univ. of Nottingham","year":"2004","author":"Backhouse R.C.","key":"e_1_3_2_1_5_1"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359579"},{"volume-title":"Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions. Texts in theoretical computer science","year":"2004","author":"Bertot Y.","key":"e_1_3_2_1_7_1"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/248932"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ITHET.2005.1560330"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581698"},{"key":"e_1_3_2_1_11_1","first-page":"166","volume-title":"ETAPS'2001","author":"Cirstea H.","year":"2001"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.10.019"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_20"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2004.12.004"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"J.-C.\n      Filli\u00e2tre\n     and \n      C.\n      March\u00e9\n  . \n  The Why\/Krakatoa\/Caduceus platform for deductive program verification\n  . In W. Damm and H. Hermanns editors CAV volume \n  4590\n   of \n  LNCS pages \n  173\n  --\n  177\n  . \n  Springer 2007\n  .]]   J.-C. Filli\u00e2tre and C. March\u00e9. The Why\/Krakatoa\/Caduceus platform for deductive program verification. In W. Damm and H. Hermanns editors CAV volume 4590 of LNCS pages 173--177. Springer 2007.]]","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"e_1_3_2_1_17_1","unstructured":"P.J.\n      Freyd\n     and \n      A.\n      \u0160\u010dedrov. Categories Allegories volume \n  39\n   of \n  Mathematical Library\n  . \n  North-Holland 1990\n  .]]  P.J. Freyd and A. \u0160\u010dedrov. Categories Allegories volume 39 of Mathematical Library. North-Holland 1990.]]"},{"volume-title":"February","year":"2008","author":"Hinze R.","key":"e_1_3_2_1_18_1"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_3"},{"volume-title":"Software abstractions: logic, language, and analysis","year":"2006","author":"Jackson D.","key":"e_1_3_2_1_20_1"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"M. P.\n      Jones\n    .\n  Functional programming with overloading and higher-order polymorphism\n  . In Johan Jeuring and Erik Meijer editors AFP'95 volume \n  925\n   of \n  LNCS pages \n  97\n  --\n  136\n  . \n  Springer 1995\n  .]]   M. P. Jones. Functional programming with overloading and higher-order polymorphism. In Johan Jeuring and Erik Meijer editors AFP'95 volume 925 of LNCS pages 97--136. Springer 1995.]]","DOI":"10.1007\/3-540-59451-5_4"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/645773.668095"},{"volume-title":"Electronic Notes in Theoretical Computer Science","year":"2000","author":"Clavel P. Lincoln M.","key":"e_1_3_2_1_24_1"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_3_2_1_27_1","first-page":"139","volume-title":"GTTSE 2007 Proceedings","author":"Oliveira J.N.","year":"2007"},{"key":"e_1_3_2_1_28_1","series-title":"LNCS","first-page":"334","volume-title":"MPC'04","author":"Oliveira J.N.","year":"2004"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"crossref","unstructured":"O. Ore. Galois connexions 1944. Trans. Amer. Math. Soc. 55:493--513.]]  O. Ore. Galois connexions 1944. Trans. Amer. Math. Soc. 55:493--513.]]","DOI":"10.1090\/S0002-9947-1944-0010555-7"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803003010"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1992.185537"},{"volume-title":"GADTs + Extensible Kinds = Dependent Programming. Technical report","year":"2005","author":"Sheard T.","key":"e_1_3_2_1_33_1"},{"volume-title":"CCTC","year":"2008","author":"Silva P.F.","key":"e_1_3_2_1_35_1"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/61690"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1090\/coll\/041"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380090105"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"crossref","unstructured":"E.\n      Visser\n    .\n  Stratego: A language for program transformation based on rewriting strategies. System description of Stratego 0.5\n  . In A. Middeldorp editor RTA volume \n  2051\n   of \n  LNCS pages \n  357\n  --\n  361\n  . \n  Springer May \n  2001\n  .]]   E. Visser. Stratego: A language for program transformation based on rewriting strategies. System description of Stratego 0.5. In A. Middeldorp editor RTA volume 2051 of LNCS pages 357--361. Springer May 2001.]]","DOI":"10.1007\/3-540-45127-7_27"},{"key":"e_1_3_2_1_40_1","series-title":"ENTCS","volume-title":"A Core Language for Rewriting","author":"Visser E.","year":"1998"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91592"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"}],"event":{"name":"PPDP08: Principles and Practice of Declarative Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"],"location":"Valencia Spain","acronym":"PPDP08"},"container-title":["Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1389449.1389456","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1389449.1389456","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:57:38Z","timestamp":1750255058000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1389449.1389456"}},"subtitle":["functional prototype of a Galois-connection based proof assistant"],"short-title":[],"issued":{"date-parts":[[2008,7,15]]},"references-count":38,"alternative-id":["10.1145\/1389449.1389456","10.1145\/1389449"],"URL":"https:\/\/doi.org\/10.1145\/1389449.1389456","relation":{},"subject":[],"published":{"date-parts":[[2008,7,15]]},"assertion":[{"value":"2008-07-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}