{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T20:13:45Z","timestamp":1758053625692,"version":"3.44.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032041661","type":"print"},{"value":"9783032041678","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,15]],"date-time":"2025-09-15T00:00:00Z","timestamp":1757894400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Modern SMT solvers can generate proofs of unsatisfiability so that the result can be checked independently. A dependable approach to verify these proofs is to reconstruct them within a proof assistant. In previous work, the SMT checker Carcara was extended to reconstruct SMT proofs in Lambdapi\u2014a proof assistant designed for interoperability, supporting the import and export of proofs for integration with other proof assistants such as Rocq, Lean, or HOL-Light. Whereas that work was limited to SMT theories without arithmetic, we here present an extension that enables the reconstruction of SMT proofs involving linear integer arithmetic.<\/jats:p>","DOI":"10.1007\/978-3-032-04167-8_20","type":"book-chapter","created":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:33Z","timestamp":1757887413000},"page":"367-385","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Checking Linear Integer Arithmetic Proofs in\u00a0Lambdapi"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-3580-2075","authenticated-orcid":false,"given":"Alessio","family":"Coltellacci","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0974-1844","authenticated-orcid":false,"given":"Stephan","family":"Merz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,15]]},"reference":[{"key":"20_CR1","doi-asserted-by":"publisher","unstructured":"Andreotti, B., Lachnitt, H., Barbosa, H.: Carcara: an efficient proof checker and elaborator for SMT proofs in the Alethe format. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13993, pp. 367\u2013386. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_19","DOI":"10.1007\/978-3-031-30823-9_19"},{"key":"20_CR2","unstructured":"Barbosa, H., Fleury, M., Fontaine, P., Schurr, H.J.: The Alethe proof format an evolving specification and reference (2024). https:\/\/verit.gitlabpages.uliege.be\/alethe\/specification.pdf"},{"key":"20_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB standard: version 2.7. Technical report, Department of Computer Science, The University of Iowa (2017\u20132024). https:\/\/smt-lib.org\/papers\/smt-lib-reference-v2.7-r2025-07-07.pdf"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-74464-1_4","volume-title":"Types for Proofs and Programs","author":"F Besson","year":"2007","unstructured":"Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 48\u201362. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74464-1_4"},{"key":"20_CR5","unstructured":"Blanqui, F.: Type safety of rewrite rules in dependent types. In: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0167, pp. 13:1\u201313:14 (2020)"},{"key":"20_CR6","unstructured":"Blanqui, F.: Encoding type universes without using matching modulo associativity and commutativity. In: Felty, A.P. (ed.) 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0228, pp. 24:1\u201324:14 (2022)"},{"key":"20_CR7","unstructured":"Blanqui, F., Dowek, G., Grienenberger, E., Hondet, G., Thir\u00e9, F.: Some axioms for mathematics. In: 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0195, pp. 20:1\u201320:19. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2021)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-71316-6_8","volume-title":"Programming Languages and Systems","author":"F Blanqui","year":"2007","unstructured":"Blanqui, F., Hardin, T., Weis, P.: On the implementation of construction functions for non-free concrete data types. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 95\u2013109. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_8"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Blanqui, F.: Translating HOL-light proofs to Coq. In: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol.\u00a0100, pp. 1\u201318 (2024)","DOI":"10.29007\/6k4x"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BFb0014565","volume-title":"Theoretical Aspects of Computer Software","author":"S Boutin","year":"1997","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 515\u2013529. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0014565"},{"key":"20_CR11","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1016\/J.JSC.2019.07.021","volume":"100","author":"M Bromberger","year":"2020","unstructured":"Bromberger, M., Sturm, T., Weidenbach, C.: A complete and terminating approach to linear integer solving. J. Symb. Comput. 100, 102\u2013136 (2020). https:\/\/doi.org\/10.1016\/J.JSC.2019.07.021","journal-title":"J. Symb. Comput."},{"key":"20_CR12","unstructured":"Coltellacci, A., Merz, S., Dowek, G.: Reconstruction of SMT proofs with Lambdapi. In: Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories Co-located with the 36th International Conference on Computer Aided Verification (CAV 2024). CEUR Workshop Proceedings, vol.\u00a03725, pp. 13\u201323. CEUR-WS.org, Montreal (2024)"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-73228-0_9","volume-title":"Typed Lambda Calculi and Applications","author":"D Cousineau","year":"2007","unstructured":"Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-pi-calculus modulo. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 102\u2013117. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73228-0_9"},{"key":"20_CR14","unstructured":"Dutertre, B., de Moura, L.: Integrating simplex with DPLL(T). Technical report CSL-06-01, SRI International (2006). https:\/\/yices.csl.sri.com\/papers\/sri-csl-06-01.pdf"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-319-08587-6_13","volume-title":"Automated Reasoning","author":"J Giesl","year":"2014","unstructured":"Giesl, J., et al.: Proving termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 184\u2013191. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_13"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11541868_7","volume-title":"Theorem Proving in Higher Order Logics","author":"B Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98\u2013113. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11541868_7"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Harper, R., Honsell, F., Plotkin, G.D.: A framework for defining logics. J. ACM 40, 143\u2013184 (1993). https:\/\/api.semanticscholar.org\/CorpusID:13375103","DOI":"10.1145\/138027.138060"},{"key":"20_CR18","unstructured":"Hondet, G., Blanqui, F.: The new rewriting engine of Dedukti. In: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0167, pp. 35:1\u201335:16. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2020)"},{"key":"20_CR19","unstructured":"Martin-L\u00f6f, P.: Intuitionistic type theory (1980)"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"20_CR21","doi-asserted-by":"publisher","unstructured":"N\u00f6tzli, A., Barbosa, H., Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Reconstructing fine-grained proofs of rewrites using a domain-specific language. In: FMCAD 2022, pp. 65\u201374 (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_12","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_12"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis. In: Proceedings of the 1991 ACM\/IEEE Conference on Supercomputing, pp. 4\u201313 (1991)","DOI":"10.1145\/125826.125848"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-030-79876-5_26","volume-title":"Automated Deduction \u2013 CADE 28","author":"H-J Schurr","year":"2021","unstructured":"Schurr, H.-J., Fleury, M., Desharnais, M.: Reliable reconstruction of fine-grained proofs in a proof assistant. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 450\u2013467. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_26"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Schurr, H.J., Fleury, M., Barbosa, H., Fontaine, P.: Alethe: towards a generic SMT proof format (extended abstract). In: Electronic Proceedings in Theoretical Computer Science, vol. 336, pp. 49\u201354 (2021)","DOI":"10.4204\/EPTCS.336.6"},{"key":"20_CR25","unstructured":"Tange, O.: GNU parallel 20250322 (2025). https:\/\/doi.org\/10.5281\/zenodo.15071920. GNU Parallel is a general parallelizer to run multiple serial command line programs in parallel without changing them"},{"key":"20_CR26","unstructured":"The Rocq Development Team: The Rocq reference manual \u2013 release 9.0.0 (2025). https:\/\/rocq-prover.org\/doc\/V9.0.0\/refman\/index.html"},{"key":"20_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/978-3-642-22438-6_38","volume-title":"Automated Deduction \u2013 CADE-23","author":"H Zankl","year":"2011","unstructured":"Zankl, H., Felgenhauer, B., Middeldorp, A.: CSI \u2013 a confluence tool. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 499\u2013505. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_38"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-04167-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,14]],"date-time":"2025-09-14T22:03:37Z","timestamp":1757887417000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-04167-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,15]]},"ISBN":["9783032041661","9783032041678"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-04167-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,15]]},"assertion":[{"value":"15 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/frocos\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}