{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T09:40:09Z","timestamp":1770370809027,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,10,22]],"date-time":"2023-10-22T00:00:00Z","timestamp":1697932800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NOvaLincs\/BASE","award":["101093006"],"award-info":[{"award-number":["101093006"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,10,22]]},"DOI":"10.1145\/3610612.3610621","type":"proceedings-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T23:13:48Z","timestamp":1697498028000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Intuitionistic Metric Temporal Logic"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-5731-2224","authenticated-orcid":false,"given":"Luiz","family":"De S\u00e1","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0746-7514","authenticated-orcid":false,"given":"Bernardo","family":"Toninho","sequence":"additional","affiliation":[{"name":"Universidade Nova de Lisboa and NOVA-LINCS, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8279-5817","authenticated-orcid":false,"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,10,22]]},"reference":[{"key":"e_1_3_2_1_1_1","article-title":"Intuitionistic Linear Temporal Logics","volume":"21","author":"Balbiani Philippe","year":"2019","unstructured":"Philippe Balbiani , Joseph Boudou , Martn Di\u00e9guez , and David Fern\u00e1ndez-Duque . 2019 . Intuitionistic Linear Temporal Logics . ACM Trans. Comput. Logic 21 , 2, Article 14 (dec 2019), 32\u00a0pages. https:\/\/doi.org\/10.1145\/3365833 10.1145\/3365833 Philippe Balbiani, Joseph Boudou, Martn Di\u00e9guez, and David Fern\u00e1ndez-Duque. 2019. Intuitionistic Linear Temporal Logics. ACM Trans. Comput. Logic 21, 2, Article 14 (dec 2019), 32\u00a0pages. https:\/\/doi.org\/10.1145\/3365833","journal-title":"ACM Trans. Comput. Logic"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1002\/malq.201700036","article-title":"A two-dimensional metric temporal logic","volume":"66","author":"Baratella Stefano","year":"2020","unstructured":"Stefano Baratella and Andrea Masini . 2020 . A two-dimensional metric temporal logic . Mathematical Logic Quarterly 66 , 1 (2020), 7 \u2013 19 . https:\/\/doi.org\/10.1002\/malq.201700036 10.1002\/malq.201700036 Stefano Baratella and Andrea Masini. 2020. A two-dimensional metric temporal logic. Mathematical Logic Quarterly 66, 1 (2020), 7\u201319. https:\/\/doi.org\/10.1002\/malq.201700036","journal-title":"Mathematical Logic Quarterly"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/349194.349197","article-title":"Temporal Logics for Real-Time System Specification","volume":"32","author":"Bellini P.","year":"2000","unstructured":"P. Bellini , R. Mattolini , and P. Nesi . 2000 . Temporal Logics for Real-Time System Specification . ACM Comput. Surv. 32 , 1 (mar 2000), 12\u201342. https:\/\/doi.org\/10.1145\/349194.349197 10.1145\/349194.349197 P. Bellini, R. Mattolini, and P. Nesi. 2000. Temporal Logics for Real-Time System Specification. ACM Comput. Surv. 32, 1 (mar 2000), 12\u201342. https:\/\/doi.org\/10.1145\/349194.349197","journal-title":"ACM Comput. Surv."},{"key":"#cr-split#-e_1_3_2_1_4_1.1","doi-asserted-by":"crossref","unstructured":"J. Bhasker and Rakesh Chadha. 2009. STA Concepts. Springer US Boston MA 15-42. https:\/\/doi.org\/10.1007\/978-0-387-93820-2_2 10.1007\/978-0-387-93820-2_2","DOI":"10.1007\/978-0-387-93820-2_2"},{"key":"#cr-split#-e_1_3_2_1_4_1.2","doi-asserted-by":"crossref","unstructured":"J. Bhasker and Rakesh Chadha. 2009. STA Concepts. Springer US Boston MA 15-42. https:\/\/doi.org\/10.1007\/978-0-387-93820-2_2","DOI":"10.1007\/978-0-387-93820-2_2"},{"key":"e_1_3_2_1_5_1","first-page":"223","article-title":"Hardware Specification with Temporal Logic: An Example","volume":"3","year":"1982","unstructured":"Bochmann. 1982 . Hardware Specification with Temporal Logic: An Example . IEEE Trans. Comput. C-31 , 3 (1982), 223 \u2013 231 . https:\/\/doi.org\/10.1109\/TC.1982.1675978 10.1109\/TC.1982.1675978 Bochmann. 1982. Hardware Specification with Temporal Logic: An Example. IEEE Trans. Comput. C-31, 3 (1982), 223\u2013231. https:\/\/doi.org\/10.1109\/TC.1982.1675978","journal-title":"IEEE Trans. Comput. C-31"},{"key":"e_1_3_2_1_6_1","volume-title":"26th EACSL Annual Conference on Computer Science Logic (CSL 2017)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a082)","author":"Boudou Joseph","year":"2017","unstructured":"Joseph Boudou , Mart\u00edn Di\u00e9guez , and David Fern\u00e1ndez-Duque . 2017 . A Decidable Intuitionistic Temporal Logic . In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a082) , Valentin Goranko and Mads Dam (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 14:1\u201314:17. https:\/\/doi.org\/10.4230\/LIPIcs.CSL. 2017.14 10.4230\/LIPIcs.CSL.2017.14 Joseph Boudou, Mart\u00edn Di\u00e9guez, and David Fern\u00e1ndez-Duque. 2017. A Decidable Intuitionistic Temporal Logic. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)(Leibniz International Proceedings in Informatics (LIPIcs), Vol.\u00a082), Valentin Goranko and Mads Dam (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 14:1\u201314:17. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2017.14"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1017\/S1471068421000089","article-title":"Exploring the Jungle of Intuitionistic Temporal Logics","volume":"21","author":"Boudou Joseph","year":"2021","unstructured":"Joseph Boudou , Mart\u00edn D\u00e9guez , David Fern\u00e1ndez-Duque , and Philip Kremer . 2021 . Exploring the Jungle of Intuitionistic Temporal Logics . Theory and Practice of Logic Programming 21 , 4 (2021), 459 \u2013 492 . https:\/\/doi.org\/10.1017\/S1471068421000089 10.1017\/S1471068421000089 Joseph Boudou, Mart\u00edn D\u00e9guez, David Fern\u00e1ndez-Duque, and Philip Kremer. 2021. Exploring the Jungle of Intuitionistic Temporal Logics. Theory and Practice of Logic Programming 21, 4 (2021), 459\u2013492. https:\/\/doi.org\/10.1017\/S1471068421000089","journal-title":"Theory and Practice of Logic Programming"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/S0304-3975(97)00139-4","article-title":"Programming in metric temporal logic","volume":"202","author":"Brzoska Christoph","year":"1998","unstructured":"Christoph Brzoska . 1998 . Programming in metric temporal logic . Theoretical Computer Science 202 , 1 (1998), 55 \u2013 125 . https:\/\/doi.org\/10.1016\/S0304-3975(97)00139-4 10.1016\/S0304-3975(97)00139-4 Christoph Brzoska. 1998. Programming in metric temporal logic. Theoretical Computer Science 202, 1 (1998), 55\u2013125. https:\/\/doi.org\/10.1016\/S0304-3975(97)00139-4","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_2_1_9_1","volume-title":"CONCUR 2010 - Concurrency Theory, Paul Gastin and Fran\u00e7ois Laroussinie (Eds.). Springer Berlin Heidelberg","author":"Caires Lu\u00eds","year":"2010","unstructured":"Lu\u00eds Caires and Frank Pfenning . 2010 . Session Types as Intuitionistic Linear Propositions . In CONCUR 2010 - Concurrency Theory, Paul Gastin and Fran\u00e7ois Laroussinie (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg, 222\u2013236. Lu\u00eds Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In CONCUR 2010 - Concurrency Theory, Paul Gastin and Fran\u00e7ois Laroussinie (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 222\u2013236."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","first-page":"584","DOI":"10.1073\/pnas.20.11.584","article-title":"Functionality in Combinatory Logic","volume":"20","author":"Curry B.","year":"1934","unstructured":"H.\u00a0 B. Curry . 1934 . Functionality in Combinatory Logic . Proceedings of the National Academy of Sciences of the United States of America 20 , 11 (1934), 584 \u2013 590 . http:\/\/www.jstor.org\/stable\/86796 H.\u00a0B. Curry. 1934. Functionality in Combinatory Logic. Proceedings of the National Academy of Sciences of the United States of America 20, 11 (1934), 584\u2013590. http:\/\/www.jstor.org\/stable\/86796","journal-title":"Proceedings of the National Academy of Sciences of the United States of America"},{"key":"e_1_3_2_1_11_1","volume-title":"Proc. ACM Program. Lang. 2, ICFP, Article 91 (jul","author":"Das Ankush","year":"2018","unstructured":"Ankush Das , Jan Hoffmann , and Frank Pfenning . 2018 . Parallel Complexity Analysis with Temporal Session Types . Proc. ACM Program. Lang. 2, ICFP, Article 91 (jul 2018), 30\u00a0pages. https:\/\/doi.org\/10.1145\/3236786 10.1145\/3236786 Ankush Das, Jan Hoffmann, and Frank Pfenning. 2018. Parallel Complexity Analysis with Temporal Session Types. Proc. ACM Program. Lang. 2, ICFP, Article 91 (jul 2018), 30\u00a0pages. https:\/\/doi.org\/10.1145\/3236786"},{"key":"e_1_3_2_1_12_1","volume-title":"Rast: A Language for Resource-Aware Session Types. Logical Methods in Computer Science","author":"Das Ankush","year":"2022","unstructured":"Ankush Das and Frank Pfenning . 2022 . Rast: A Language for Resource-Aware Session Types. Logical Methods in Computer Science Volume 18 , Issue 1 (Jan. 2022), 9:1\u20139:36. https:\/\/doi.org\/10.46298\/lmcs-18(1:9)2022 10.46298\/lmcs-18(1:9)2022 Ankush Das and Frank Pfenning. 2022. Rast: A Language for Resource-Aware Session Types. Logical Methods in Computer Science Volume 18, Issue 1 (Jan. 2022), 9:1\u20139:36. https:\/\/doi.org\/10.46298\/lmcs-18(1:9)2022"},{"key":"e_1_3_2_1_13_1","volume-title":"Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science(LICS \u201996)","author":"Davies R.","year":"1996","unstructured":"R. Davies . 1996 . A Temporal-Logic Approach to Binding-Time Analysis . In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science(LICS \u201996) . IEEE Computer Society, USA, 184\u2013195. https:\/\/doi.org\/10.1109\/LICS. 1996.561317 10.1109\/LICS.1996.561317 R. Davies. 1996. A Temporal-Logic Approach to Binding-Time Analysis. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science(LICS \u201996). IEEE Computer Society, USA, 184\u2013195. https:\/\/doi.org\/10.1109\/LICS.1996.561317"},{"key":"e_1_3_2_1_14_1","article-title":"A Temporal Logic Approach to Binding-Time Analysis","volume":"64","author":"Davies Rowan","year":"2017","unstructured":"Rowan Davies . 2017 . A Temporal Logic Approach to Binding-Time Analysis . Journal of the ACM 64 , 1 (2017), 1:1\u20131:45. Rowan Davies. 2017. A Temporal Logic Approach to Binding-Time Analysis. Journal of the ACM 64, 1 (2017), 1:1\u20131:45.","journal-title":"Journal of the ACM"},{"key":"e_1_3_2_1_15_1","first-page":"1308","article-title":"Mathematical Intuitionism. Introduction to Proof Theory","volume":"55","author":"Dragalin G.","year":"1990","unstructured":"A.\u00a0 G. Dragalin and E. Mendelson . 1990 . Mathematical Intuitionism. Introduction to Proof Theory . Journal of Symbolic Logic 55 , 3 (1990), 1308 \u2013 1309 . https:\/\/doi.org\/10.2307\/2274493 10.2307\/2274493 A.\u00a0G. Dragalin and E. Mendelson. 1990. Mathematical Intuitionism. Introduction to Proof Theory. Journal of Symbolic Logic 55, 3 (1990), 1308\u20131309. https:\/\/doi.org\/10.2307\/2274493","journal-title":"Journal of Symbolic Logic"},{"key":"e_1_3_2_1_16_1","volume-title":"The Logical Basis of Metaphysics","author":"Dummett Michael","unstructured":"Michael Dummett . 1991. The Logical Basis of Metaphysics . Cambridge, Mass .: Harvard University Press . Michael Dummett. 1991. The Logical Basis of Metaphysics. Cambridge, Mass.: Harvard University Press."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/j.entcs.2009.07.016","article-title":"On Metric Temporal \u0141ukasiewicz Logic","volume":"246","author":"Flaminio Tommaso","year":"2009","unstructured":"Tommaso Flaminio and Elisa\u00a0 B.P. Tiezzi . 2009 . On Metric Temporal \u0141ukasiewicz Logic . Electronic Notes in Theoretical Computer Science 246 (2009), 71 \u2013 85 . https:\/\/doi.org\/10.1016\/j.entcs.2009.07.016 Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008). 10.1016\/j.entcs.2009.07.016 Tommaso Flaminio and Elisa\u00a0B.P. Tiezzi. 2009. On Metric Temporal \u0141ukasiewicz Logic. Electronic Notes in Theoretical Computer Science 246 (2009), 71\u201385. https:\/\/doi.org\/10.1016\/j.entcs.2009.07.016 Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008).","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen Gerhard","year":"1935","unstructured":"Gerhard Gentzen . 1935 . Untersuchungen \u00fcber das logische Schlie\u00dfen . I. Mathematische Zeitschrift 39 , 1 (1935), 176 \u2013 210 . https:\/\/doi.org\/10.1007\/BF01201353 10.1007\/BF01201353 Gerhard Gentzen. 1935. Untersuchungen \u00fcber das logische Schlie\u00dfen. I. Mathematische Zeitschrift 39, 1 (1935), 176\u2013210. https:\/\/doi.org\/10.1007\/BF01201353","journal-title":"I. Mathematische Zeitschrift"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear Logic","volume":"50","author":"Girard Jean-Yves","year":"1987","unstructured":"Jean-Yves Girard . 1987 . Linear Logic . Theoretical Computer Science 50 (1987), 1 \u2013 102 . Jean-Yves Girard. 1987. Linear Logic. Theoretical Computer Science 50 (1987), 1\u2013102.","journal-title":"Theoretical Computer Science"},{"key":"e_1_3_2_1_20_1","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Haskell Curry, Hindley B., Seldin\u00a0J. Roger, and P.\u00a0Jonathan (Eds.)","author":"Howard William\u00a0Alvin","unstructured":"William\u00a0Alvin Howard . 1980. The Formulae-as-Types Notion of Construction . In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Haskell Curry, Hindley B., Seldin\u00a0J. Roger, and P.\u00a0Jonathan (Eds.) . Academic Press . William\u00a0Alvin Howard. 1980. The Formulae-as-Types Notion of Construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Haskell Curry, Hindley B., Seldin\u00a0J. Roger, and P.\u00a0Jonathan (Eds.). Academic Press."},{"key":"e_1_3_2_1_21_1","volume-title":"Vehicle Routing Problem with Metric Temporal Logic Specifications. In 2008 47th IEEE Conference on Decision and Control. 3953\u20133958","author":"Karaman Sertac","year":"2008","unstructured":"Sertac Karaman and Emilio Frazzoli . 2008 . Vehicle Routing Problem with Metric Temporal Logic Specifications. In 2008 47th IEEE Conference on Decision and Control. 3953\u20133958 . https:\/\/doi.org\/10.1109\/CDC.2008.4739366 10.1109\/CDC.2008.4739366 Sertac Karaman and Emilio Frazzoli. 2008. Vehicle Routing Problem with Metric Temporal Logic Specifications. In 2008 47th IEEE Conference on Decision and Control. 3953\u20133958. https:\/\/doi.org\/10.1109\/CDC.2008.4739366"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","first-page":"1491","DOI":"10.1016\/j.ic.2010.09.008","article-title":"Constructive linear-time temporal logic: Proof systems and Kripke semantics","volume":"209","author":"Kojima Kensuke","year":"2011","unstructured":"Kensuke Kojima and Atsushi Igarashi . 2011 . Constructive linear-time temporal logic: Proof systems and Kripke semantics . Information and Computation 209 , 12 (2011), 1491 \u2013 1503 . https:\/\/doi.org\/10.1016\/j.ic.2010.09.008 Intuitionistic Modal Logic and Applications (IMLA 2008). 10.1016\/j.ic.2010.09.008 Kensuke Kojima and Atsushi Igarashi. 2011. Constructive linear-time temporal logic: Proof systems and Kripke semantics. Information and Computation 209, 12 (2011), 1491\u20131503. https:\/\/doi.org\/10.1016\/j.ic.2010.09.008 Intuitionistic Modal Logic and Applications (IMLA 2008).","journal-title":"Information and Computation"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BF01995674","article-title":"Specifying real-time properties with metric temporal logic","volume":"2","author":"Koymans Ron","year":"1990","unstructured":"Ron Koymans . 1990 . Specifying real-time properties with metric temporal logic . Real-Time Systems 2 , 4 (1990), 255 \u2013 299 . https:\/\/doi.org\/10.1007\/BF01995674 10.1007\/BF01995674 Ron Koymans. 1990. Specifying real-time properties with metric temporal logic. Real-Time Systems 2, 4 (1990), 255\u2013299. https:\/\/doi.org\/10.1007\/BF01995674","journal-title":"Real-Time Systems"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","article-title":"The temporal logic of actions","volume":"16","author":"Lamport Leslie","year":"1994","unstructured":"Leslie Lamport . 1994 . The temporal logic of actions . ACM Transactions on Programming Languages and Systems (TOPLAS) 16 , 3 (1994), 872 \u2013 923 . Leslie Lamport. 1994. The temporal logic of actions. ACM Transactions on Programming Languages and Systems (TOPLAS) 16, 3 (1994), 872\u2013923.","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"e_1_3_2_1_25_1","first-page":"11","article-title":"On the Meanings of the Logical Constants and the Justifications of the Logical Laws","volume":"1","author":"Martin-L\u00f6f Per","year":"1996","unstructured":"Per Martin-L\u00f6f . 1996 . On the Meanings of the Logical Constants and the Justifications of the Logical Laws . Nordic Journal of Philosophical Logic 1 , 1 (1996), 11 \u2013 60 . Per Martin-L\u00f6f. 1996. On the Meanings of the Logical Constants and the Justifications of the Logical Laws. Nordic Journal of Philosophical Logic 1, 1 (1996), 11\u201360.","journal-title":"Nordic Journal of Philosophical Logic"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/MC.1985.1662795","article-title":"A Temporal Logic for Multilevel Reasoning about Hardware","volume":"18","year":"1985","unstructured":"Moszkowski. 1985 . A Temporal Logic for Multilevel Reasoning about Hardware . Computer 18 , 2 (1985), 10 \u2013 19 . https:\/\/doi.org\/10.1109\/MC.1985.1662795 10.1109\/MC.1985.1662795 Moszkowski. 1985. A Temporal Logic for Multilevel Reasoning about Hardware. Computer 18, 2 (1985), 10\u201319. https:\/\/doi.org\/10.1109\/MC.1985.1662795","journal-title":"Computer"},{"key":"e_1_3_2_1_27_1","volume-title":"20th Annual IEEE Symposium on Logic in Computer Science (LICS\u2019 05)","author":"Ouaknine J.","year":"2005","unstructured":"J. Ouaknine and J. Worrell . 2005. On the decidability of metric temporal logic . In 20th Annual IEEE Symposium on Logic in Computer Science (LICS\u2019 05) . 188\u2013197. https:\/\/doi.org\/10.1109\/LICS. 2005 .33 10.1109\/LICS.2005.33 J. Ouaknine and J. Worrell. 2005. On the decidability of metric temporal logic. In 20th Annual IEEE Symposium on Logic in Computer Science (LICS\u2019 05). 188\u2013197. https:\/\/doi.org\/10.1109\/LICS.2005.33"},{"key":"e_1_3_2_1_28_1","volume-title":"Foundations of Software Science and Computation Structures, Luca Aceto and Anna Ing\u00f3lfsd\u00f3ttir (Eds.)","author":"Ouaknine Jo\u00ebl","unstructured":"Jo\u00ebl Ouaknine and James Worrell . 2006. On Metric Temporal Logic and Faulty Turing Machines . In Foundations of Software Science and Computation Structures, Luca Aceto and Anna Ing\u00f3lfsd\u00f3ttir (Eds.) . Springer Berlin Heidelberg, Berlin , Heidelberg , 217\u2013230. https:\/\/doi.org\/10.1007\/11690634_15 10.1007\/11690634_15 Jo\u00ebl Ouaknine and James Worrell. 2006. On Metric Temporal Logic and Faulty Turing Machines. In Foundations of Software Science and Computation Structures, Luca Aceto and Anna Ing\u00f3lfsd\u00f3ttir (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 217\u2013230. https:\/\/doi.org\/10.1007\/11690634_15"},{"key":"e_1_3_2_1_29_1","volume-title":"18th Annual Symposium on Foundations of Computer Science (sfcs 1977","author":"Pnueli Amir","year":"1977","unstructured":"Amir Pnueli . 1977 . The temporal logic of programs . In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977 ). 46\u201357. https:\/\/doi.org\/10.1109\/SFCS.1977.32 10.1109\/SFCS.1977.32 Amir Pnueli. 1977. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977). 46\u201357. https:\/\/doi.org\/10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_30_1","volume-title":"Natural Deduction: A Proof-Theoretical Study.","author":"Prawitz Dag","year":"1965","unstructured":"Dag Prawitz . 1965 . Natural Deduction: A Proof-Theoretical Study. Stockholm, Sweden : Dover Publications . Dag Prawitz. 1965. Natural Deduction: A Proof-Theoretical Study. Stockholm, Sweden: Dover Publications."},{"key":"e_1_3_2_1_31_1","first-page":"1","article-title":"Meaning and Proofs","volume":"43","author":"Prawitz Dag","year":"1977","unstructured":"Dag Prawitz . 1977 . Meaning and Proofs : On the Conflict Between Classical and Intuitionistic Logic. Theroia 43 (1977), 1 \u2013 40 . Dag Prawitz. 1977. Meaning and Proofs: On the Conflict Between Classical and Intuitionistic Logic. Theroia 43 (1977), 1\u201340.","journal-title":"On the Conflict Between Classical and Intuitionistic Logic. Theroia"},{"key":"e_1_3_2_1_32_1","volume-title":"The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.\u00a0D. Dissertation","author":"Simpson K","unstructured":"Alex\u00a0 K Simpson . 1994. The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.\u00a0D. Dissertation . University of Edinburgh. Alex\u00a0K Simpson. 1994. The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.\u00a0D. Dissertation. University of Edinburgh."}],"event":{"name":"PPDP 2023: International Symposium on Principles and Practice of Declarative Programming","location":"Lisboa Portugal","acronym":"PPDP 2023"},"container-title":["International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3610612.3610621","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:36:00Z","timestamp":1750178160000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3610612.3610621"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,22]]},"references-count":33,"alternative-id":["10.1145\/3610612.3610621","10.1145\/3610612"],"URL":"https:\/\/doi.org\/10.1145\/3610612.3610621","relation":{},"subject":[],"published":{"date-parts":[[2023,10,22]]},"assertion":[{"value":"2023-10-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}