{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T08:59:28Z","timestamp":1776848368940,"version":"3.51.2"},"reference-count":23,"publisher":"IEEE","license":[{"start":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T00:00:00Z","timestamp":1761523200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T00:00:00Z","timestamp":1761523200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,10,27]]},"DOI":"10.1109\/clei67442.2025.11420557","type":"proceedings-article","created":{"date-parts":[[2026,4,21]],"date-time":"2026-04-21T19:46:49Z","timestamp":1776800809000},"page":"1-10","source":"Crossref","is-referenced-by-count":0,"title":["CalcLogic: Functional Implementation of an Interactive Proof Assistant for Dijkstra-Scholten Calculational Logic"],"prefix":"10.1109","author":[{"given":"Federico","family":"Flaviani","sequence":"first","affiliation":[{"name":"Universidad Simón Bolívar,Departamento de Computación y Tecnología de la Información,Caracas,Venezuela"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonardo","family":"L\u00f3pez","sequence":"additional","affiliation":[{"name":"Universidad Simón Bolívar,Departamento de Computación y Tecnología de la Información,Caracas,Venezuela"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ronald","family":"Becerra","sequence":"additional","affiliation":[{"name":"Universidad Simón Bolívar,Departamento de Computación y Tecnología de la Información,Caracas,Venezuela"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jorge","family":"Baralt-Torrijos","sequence":"additional","affiliation":[{"name":"Universidad Simón Bolívar,Departamento de Computación y Tecnología de la Información,Caracas,Venezuela"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3837-7"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"ref4","article-title":"Formalizations of substitution of equals for equals","volume-title":"Technical Report","author":"Gries","year":"1998"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.2307\/1968337"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_17"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_19"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_25"},{"issue":"1","key":"ref9","first-page":"43","article-title":"A basic formal equational predicate logic - Part I","volume":"29","author":"Tourlakis","year":"2000","journal-title":"Bulletin of the Section of Logic"},{"issue":"3","key":"ref10","first-page":"75","article-title":"A basic formal equational predicate logic - Part II","volume":"29","author":"Tourlakis","year":"2000","journal-title":"Bulletin of the Section of Logic"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/11.4.623"},{"key":"ref12","article-title":"The everywhere operator once more","volume-title":"Technical Report","author":"Dijkstra","year":"1990"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-60858-2_16"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-16-2834-4_14"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/clei56649.2022.9959908"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.19153\/cleiej.26.2.6"},{"key":"ref17","volume-title":"Principia Mathematica","volume":"1","author":"Russell","year":"1925"},{"key":"ref18","volume-title":"Combinatory logic","volume":"1","author":"Curry","year":"1958"},{"key":"ref19","volume-title":"Derivation and Computation: taking the Curry-Howard correspondence seriously","author":"Simmons","year":"2000"},{"key":"ref20","article-title":"A calculational proof of andrew\u2019s challenge","volume-title":"Technical Report","author":"Gries","year":"1996"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1090\/noti3041"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.2307\/1968422"},{"key":"ref23","article-title":"Begriffsschrift, 1879","volume-title":"Translated in: From Frege to Godel","author":"Frege","year":"1967"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1215\/00294527-2008-017"}],"event":{"name":"2025 LI Latin American Computer Conference (CLEI)","location":"Valpara\u00edso, Chile","start":{"date-parts":[[2025,10,27]]},"end":{"date-parts":[[2025,10,31]]}},"container-title":["2025 LI Latin American Computer Conference (CLEI)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11420220\/11420231\/11420557.pdf?arnumber=11420557","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T08:03:03Z","timestamp":1776844983000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11420557\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,27]]},"references-count":23,"URL":"https:\/\/doi.org\/10.1109\/clei67442.2025.11420557","relation":{},"subject":[],"published":{"date-parts":[[2025,10,27]]}}}