{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T04:10:29Z","timestamp":1751688629516,"version":"3.41.0"},"reference-count":52,"publisher":"Cambridge University Press (CUP)","issue":"9","license":[{"start":{"date-parts":[[2018,5,15]],"date-time":"2018-05-15T00:00:00Z","timestamp":1526342400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2018,10]]},"abstract":"<jats:p>We present two extensions of the<jats:monospace>LF<\/jats:monospace>constructive type theory featuring monadic<jats:italic>locks<\/jats:italic>. A lock is a monadic type construct that captures the effect of an<jats:italic>external call to an oracle<\/jats:italic>. Such calls are the basic tool for<jats:italic>plugging-in<\/jats:italic>and gluing together, different metalanguages and proof development environments. Oracles can be invoked either to check that a constraint holds or to provide a witness. The systems are presented in the<jats:italic>canonical style<\/jats:italic>developed by the \u2018CMU School.\u2019 The first system,<jats:monospace>CLLF<\/jats:monospace><jats:sub>\ud835\udcab<\/jats:sub>, is the canonical version of the system<jats:monospace>LLF<\/jats:monospace><jats:sub>\ud835\udcab<\/jats:sub>, presented earlier by the authors. The second system,<jats:monospace>CLLF<\/jats:monospace><jats:sub>\ud835\udcab?<\/jats:sub>, features the possibility of invoking the oracle to obtain also a witness satisfying a given constraint. In order to illustrate the advantages of our new frameworks, we show how to encode logical systems featuring rules that deeply constrain the shape of proofs. The locks mechanisms of<jats:monospace>CLLF<\/jats:monospace><jats:sub>\ud835\udcab<\/jats:sub>and<jats:monospace>CLLF<\/jats:monospace><jats:sub>\ud835\udcab?<\/jats:sub>permit to factor out naturally the complexities arising from enforcing these \u2018side conditions,\u2019 which severely obscure standard<jats:monospace>LF<\/jats:monospace>encodings. We discuss Girard's Elementary Affine Logic, Fitch\u2013Prawitz set theory, call-by-value \u03bb-calculi and functions, both total and even partial.<\/jats:p>","DOI":"10.1017\/s0960129518000105","type":"journal-article","created":{"date-parts":[[2018,5,15]],"date-time":"2018-05-15T08:46:07Z","timestamp":1526373967000},"page":"1578-1605","source":"Crossref","is-referenced-by-count":0,"title":["Plugging-in proof development environments using<i>Locks<\/i>in<tt>LF<\/tt>"],"prefix":"10.1017","volume":"28","author":[{"given":"FURIO","family":"HONSELL","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"LUIGI","family":"LIQUORI","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"PETAR","family":"MAKSIMOVI\u0106","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"IVAN","family":"SCAGNETTO","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2018,5,15]]},"reference":[{"key":"S0960129518000105_ref45","first-page":"203","volume-title":"Insolubles and Consequences : Essays in Honor of Stephen Read","author":"Schroeder-Heister","year":"2012"},{"key":"S0960129518000105_ref8","unstructured":"Boespflug M. , Carbonneaux Q. and Hermant O. (2012). The \u03bb\u03a0-calculus modulo as a universal proof language. In: Proceedings of the 2nd International Workshop on Proof Exchange for Theorem Proving (PxTP '12), vol. 878, 28\u201343, doi:10.1.1.416.1602."},{"key":"S0960129518000105_ref4","doi-asserted-by":"publisher","DOI":"10.1023\/A:1015761529444"},{"key":"#cr-split#-S0960129518000105_ref31.1","unstructured":"2. Honsell F. (2016). Wherefore art thou .??.??. semantics of computation?. In: Gadducci F., Tavosanis M."},{"key":"#cr-split#-S0960129518000105_ref31.2","unstructured":"3. (eds) History and Philosophy of Computing. HaPoC 2015. IFIP Advances in Information and Communication Technology, vol 487. Springer, Cham."},{"key":"#cr-split#-S0960129518000105_ref32.1","doi-asserted-by":"crossref","unstructured":"4. Honsell F., Liquori L., Maksimovic P. and Scagnetto I. (2017). LLF : A logical framework for modeling external evidence, side conditions, and proof irrelevance using monads. In: Proceedings of the Logical Methods in Computer Science, vol. 13","DOI":"10.23638\/LMCS-13(3:2)2017"},{"key":"#cr-split#-S0960129518000105_ref32.2","unstructured":"5. July 6, 2017, Special Issue of Logical Methods in Computer Science devoted to Festschrift for Pierre-Louis Curien."},{"key":"S0960129518000105_ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2503887.2503896"},{"key":"S0960129518000105_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2364406.2364409"},{"volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","year":"2015","author":"Chihani","key":"S0960129518000105_ref11"},{"key":"S0960129518000105_ref39","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48660-7_14"},{"key":"S0960129518000105_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/BF01203032"},{"key":"S0960129518000105_ref22","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006430"},{"key":"S0960129518000105_ref27","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/ext028"},{"key":"S0960129518000105_ref30","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.185.1"},{"key":"S0960129518000105_ref48","unstructured":"Stump A. , Reynolds A. , Tinelli C. , Laugesen A. , Eades H. , Oliver C. and Zhang R. (2012). LFSC for SMT proofs: Work in progress. In: Proceedings of the 2nd International Workshop on Proof eXchange for Theorem Proving (PxTP '12), Manchester, UK."},{"key":"S0960129518000105_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44755-5_15"},{"key":"S0960129518000105_ref42","first-page":"561","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Pottinger","year":"1980"},{"key":"S0960129518000105_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/1389449.1389469"},{"volume-title":"Symbolic Logic\u2014An Introduction","year":"1952","author":"Fitch","key":"S0960129518000105_ref19"},{"key":"S0960129518000105_ref15","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2627"},{"key":"S0960129518000105_ref37","doi-asserted-by":"crossref","unstructured":"Moggi E. (1989). Computational lambda-calculus and monads. In: Proceedings of the Lecture Notes in Computer Science (LICS '89), IEEE Press, 14\u201323. doi:10.1.1.26.2787.","DOI":"10.1109\/LICS.1989.39155"},{"key":"S0960129518000105_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028392"},{"key":"S0960129518000105_ref46","doi-asserted-by":"publisher","DOI":"10.1007\/s11245-012-9119-x"},{"key":"S0960129518000105_ref6","unstructured":"Battel C. and Felty A. (2015). A higher-order logical framework for reasoning about programming languages. In: Proceedings of the CMS Winter Meeting, Montr\u00e9al, December 4\u20137, 2015."},{"key":"S0960129518000105_ref5","doi-asserted-by":"crossref","unstructured":"Barthe G. , Cirstea H. , Kirchner C. and Liquori L. (2003). Pure pattern type systems. In: Proceedings of the 30th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'03), ACM, 250\u2013261, doi:10.1.1.298.4555.","DOI":"10.1145\/604131.604152"},{"key":"S0960129518000105_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_21"},{"key":"S0960129518000105_ref21","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2700"},{"key":"S0960129518000105_ref7","doi-asserted-by":"crossref","unstructured":"Blanco R. , Chihani Z. and Miller D. (2017). Translating between implicit and explicit versions of proof. In: de Moura L. (ed.), Proceedings of the 26th International Conference on Automated Deduction (CADE '17). Lecture Notes in Computer Science, vol. 10395, Springer, Cham.","DOI":"10.1007\/978-3-319-63046-5_16"},{"key":"S0960129518000105_ref47","doi-asserted-by":"crossref","unstructured":"Stump A. (2009). Proof checking technology for satisfiability modulo theories. In: Proceedings of the 4th International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP '08), vol. 228, 121\u2013133, doi:10.1.1.219.1459.","DOI":"10.1016\/j.entcs.2008.12.121"},{"key":"S0960129518000105_ref10","doi-asserted-by":"crossref","unstructured":"Casinghino C. , Sj\u00f6berg V. and Weirich S. (2014). Combining proofs and programs in a dependently typed language. In: Proceedings of the 41st SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14), ACM, 33\u201345.","DOI":"10.1145\/2535838.2535883"},{"key":"S0960129518000105_ref49","unstructured":"Wang Y. and Chaudhuri K. (2015). A proof-theoretic characterization of independence in type theory. In: Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA '15), vol. 38, 332\u2013346."},{"key":"S0960129518000105_ref34","doi-asserted-by":"crossref","unstructured":"Kerber M. (2006). A dynamic poincar\u00e9 principle. In: Borwein J.M. and Farmer W.M. (eds.) Proceedings of 5th International Conference on Mathematical Knowledge Management (MKM '06), Lecture Notes in Artificial Intelligence, vol. 4108, Springer, 44\u201353.","DOI":"10.1007\/11812289_5"},{"key":"S0960129518000105_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"S0960129518000105_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00095-5"},{"key":"S0960129518000105_ref9","unstructured":"Boulton R. , Gordon A. , Gordon M. , Harrison J. , Herbert J. and Van Tassel J. (1992). Experience with embedding hardware description languages in HOL. In: Proceedings of the IFIP TC10\/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience (TPCD '92), North-Holland, 129\u2013156, doi:10.1.1.111.260."},{"key":"S0960129518000105_ref36","unstructured":"Moggi E. (1988). The Partial Lambda Calculus. Ph.D. thesis, University of Edinburgh, doi:10.1.1.53.8462."},{"key":"S0960129518000105_ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_28"},{"key":"S0960129518000105_ref35","first-page":"1","volume-title":"Designing Correct Circuits","author":"Mendler","year":"1991"},{"key":"S0960129518000105_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"S0960129518000105_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.10.002"},{"key":"S0960129518000105_ref12","unstructured":"Chihani Z. and Miller D. (2016). Proof Certificates for Equality Reasoning, Electronic Notes in Theoretical Computer Science, vol. 323, 93\u2013108, ISSN 1571-0661."},{"key":"S0960129518000105_ref13","doi-asserted-by":"crossref","unstructured":"Cousineau D. and Dowek G. (2007). Embedding pure type systems in the lambda-pi-calculus modulo. In: Proceedings of the International Conference on Typed Lambda Calculi and Applications (TLCA '07), Lecture Notes in Computer Science, vol. 4583, Springer-Verlag, 102\u2013117, doi:10.1.1.102.4096.","DOI":"10.1007\/978-3-540-73228-0_9"},{"key":"S0960129518000105_ref50","unstructured":"Watkins K. , Cervesato I. , Pfenning F. and Walker D. (2002). A concurrent logical framework I: Judgments and properties. Tech. rep. CMU-CS-02-101, CMU, doi:10.1.1.14.5484."},{"key":"S0960129518000105_ref20","doi-asserted-by":"publisher","DOI":"10.21236\/ADA476728"},{"key":"S0960129518000105_ref18","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre J.-C. (2013). One logic to use them all. In: Maria Paola Bonacina (ed.) Proceedings of the 24th International Conference on Automated Deduction (CADE '13), Lake Placid, New York, NY, USA.","DOI":"10.1007\/978-3-642-38574-2"},{"volume-title":"Natural Deduction. A Proof Theoretical Study","year":"1965","author":"Prawitz","key":"S0960129518000105_ref43"},{"volume-title":"Volume in Honor of G. Plotkin","year":"2007","author":"Honsell","key":"S0960129518000105_ref25"},{"key":"S0960129518000105_ref33","doi-asserted-by":"crossref","unstructured":"Honsell F. , Lenisa M. , Liquori L. and Scagnetto I. (2016). Implementing Cantor's Paradise. In: Proceedings of 14th Asian Symposium on Programming Languages and Systems (APLAS '16), Chapter Programming Languages and Systems, Lecture Notes in Computer Science, vol. 10017, Vietnam, November 21\u201323, Springer, 229\u2013250.","DOI":"10.1007\/978-3-319-47958-3_13"},{"key":"S0960129518000105_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44522-8_28"},{"key":"S0960129518000105_ref17","unstructured":"Fairtlough M. Mendler M. and Walton M. (1997). First-order lax logic as a framework for constraint logic programming. Tech. rep. MIPS-9714, https:\/\/pdfs.semanticscholar.org\/a934\/8355b554e593e1e9e370136f1d7e268c8ba8.pdf."},{"key":"S0960129518000105_ref14","doi-asserted-by":"crossref","unstructured":"Danielsson N.A. , Hughes J. , Jansson P. and Gibbons J. (2006). Fast and loose reasoning is morally correct. In: Proceedings of the 33rd SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '06), ACM, 206\u2013217.","DOI":"10.1145\/1111037.1111056"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129518000105","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T14:51:26Z","timestamp":1751640686000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129518000105\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,15]]},"references-count":52,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2018,10]]}},"alternative-id":["S0960129518000105"],"URL":"https:\/\/doi.org\/10.1017\/s0960129518000105","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2018,5,15]]}}}