{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T09:10:16Z","timestamp":1780564216142,"version":"3.54.1"},"reference-count":47,"publisher":"Elsevier BV","issue":"9","license":[{"start":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T00:00:00Z","timestamp":1790812800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T00:00:00Z","timestamp":1790812800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T00:00:00Z","timestamp":1775692800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003141","name":"Secretariat of Science Humanities Technology and Innovation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003141","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006087","name":"National Autonomous University of Mexico Directorate General of Academic Staff Affairs","doi-asserted-by":"publisher","award":["IN101723"],"award-info":[{"award-number":["IN101723"]}],"id":[{"id":"10.13039\/501100006087","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Annals of Pure and Applied Logic"],"published-print":{"date-parts":[[2026,10]]},"DOI":"10.1016\/j.apal.2026.103768","type":"journal-article","created":{"date-parts":[[2026,4,2]],"date-time":"2026-04-02T17:26:39Z","timestamp":1775150799000},"page":"103768","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"title":["Mind the gap: A conciliating short proof of strong normalization for minimal propositional logic"],"prefix":"10.1016","volume":"177","author":[{"given":"Favio E.","family":"Miranda-Perea","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-1306-6895","authenticated-orcid":false,"given":"Eduardo","family":"Ugalde-Reyes","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.apal.2026.103768_br0010","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2007.11.009","article-title":"Normalization for the simply-typed lambda-calculus in twelf","volume":"199","author":"Abel","year":"2008","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.apal.2026.103768_br0020","series-title":"Constructions Inductive Types and Strong Normalization","author":"Alterkirch","year":"1993"},{"key":"10.1016\/j.apal.2026.103768_br0030","first-page":"2351","article-title":"The challenge of computer mathematics","volume":"363","author":"Barendregt","year":"2005","journal-title":"Philos. Trans. R. Soc. Lond. A"},{"key":"10.1016\/j.apal.2026.103768_br0040","series-title":"Types for Proofs and Programs","first-page":"50","article-title":"Extracting a normalization algorithm in Isabelle\/Hol","author":"Berghofer","year":"2006"},{"key":"10.1016\/j.apal.2026.103768_br0050","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/BF00262062","article-title":"A note on the elimination rules","volume":"6","author":"Cagnoni","year":"1977","journal-title":"J. Philos. Log."},{"key":"10.1016\/j.apal.2026.103768_br0060","series-title":"Italian Studies in the Philosophy of Science","first-page":"13","article-title":"Proof theory and theory of meaning","author":"Celluci","year":"1980"},{"key":"10.1016\/j.apal.2026.103768_br0070","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/s10817-011-9225-2","article-title":"The locally nameless representation","volume":"49","author":"Chargu\u00e9raud","year":"2011","journal-title":"J. Autom. Reason."},{"key":"10.1016\/j.apal.2026.103768_br0080","series-title":"Kontrolliertes Denken: Untersuchungen zum Logikkalk\u00fcl und zur Logik der Einzelwissenschaften","first-page":"22","article-title":"The weak theory of implication","author":"Church","year":"1951"},{"key":"10.1016\/j.apal.2026.103768_br0090","series-title":"Introduction to Mathematical Logic, vol. 1","author":"Church","year":"1956"},{"key":"10.1016\/j.apal.2026.103768_br0100","doi-asserted-by":"crossref","first-page":"509","DOI":"10.2307\/2370619","article-title":"Grundlagen der kombinatorischen logik","volume":"52","author":"Curry","year":"1930","journal-title":"Am. J. Math."},{"key":"10.1016\/j.apal.2026.103768_br0110","series-title":"Why Prove It Again? Alternative Proofs in Mathematical Practice","author":"Dawson","year":"2015"},{"key":"10.1016\/j.apal.2026.103768_br0120","first-page":"381","article-title":"Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem","volume":"75","author":"de Bruijn","year":"1972","journal-title":"Proc. K. Ned. Akad. Wet., Ser. A, Indag. Math."},{"key":"10.1016\/j.apal.2026.103768_br0130","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1023\/A:1022131513275","article-title":"Intentional gaps in mathematical proofs","volume":"134","author":"Fallis","year":"2003","journal-title":"Synthese"},{"key":"10.1016\/j.apal.2026.103768_br0140","series-title":"Begriffsschrift, Eine Der Arithmetischen Nachgebildete Formelsprachen Des Reinen Denkens","author":"Frege","year":"1879"},{"key":"10.1016\/j.apal.2026.103768_br0150","series-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","first-page":"453","article-title":"An early proof of normalization by A.M. Turing","author":"Gandy","year":"1980"},{"key":"10.1016\/j.apal.2026.103768_br0160","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische schlie\u00dfen","volume":"39","author":"Gentzen","year":"1934","journal-title":"Math. Z."},{"key":"10.1016\/j.apal.2026.103768_br0170","series-title":"Proofs and Types","author":"Girard","year":"1990"},{"key":"10.1016\/j.apal.2026.103768_br0180","first-page":"1370","article-title":"Formal proof","volume":"55","author":"Hales","year":"2008","journal-title":"Not. Am. Math. Soc."},{"key":"10.1016\/j.apal.2026.103768_br0190","series-title":"Natural Deduction, Hybrid Systems and Modal Logics","author":"Indrzejczak","year":"2010"},{"key":"10.1016\/j.apal.2026.103768_br0200","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/s00153-002-0156-9","article-title":"Short proofs of normalization for the simply-typed \u03bb-calculus, permutative conversions and G\u00f6del's T","volume":"42","author":"Joachimski","year":"2003","journal-title":"Arch. Math. Log."},{"key":"10.1016\/j.apal.2026.103768_br0210","series-title":"Logic, Part I","author":"Johnson","year":"1921"},{"key":"10.1016\/j.apal.2026.103768_br0220","doi-asserted-by":"crossref","first-page":"782","DOI":"10.2307\/2274330","article-title":"Church-rosser theorem for typed functional systems","volume":"50","author":"Koletsos","year":"1985","journal-title":"J. Symb. Log."},{"key":"10.1016\/j.apal.2026.103768_br0230","series-title":"A Survey of Symbolic Logic","author":"Lewis","year":"1918"},{"key":"10.1016\/j.apal.2026.103768_br0240","series-title":"Introduction to Proof-Theory: Normalization, Cut-Elimination, and Consistency Proofs","author":"Mancosu","year":"2021"},{"key":"10.1016\/j.apal.2026.103768_br0250","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1016\/j.apal.2004.10.009","article-title":"Non-strictly positive fixed points for classical natural deduction","volume":"133","author":"Matthes","year":"2005","journal-title":"Ann. Pure Appl. Log."},{"key":"10.1016\/j.apal.2026.103768_br0260","series-title":"Typed Lambda Calculi and Applications","first-page":"328","article-title":"Typed \u03bb-calculi with explicit substitutions may not terminate","author":"Mellies","year":"1995"},{"key":"10.1016\/j.apal.2026.103768_br0270","series-title":"Philosophy of Computing","first-page":"107","article-title":"On the conciliation of traditional proofs and computer-assisted proofs","author":"Miranda-Perea","year":"2022"},{"key":"10.1016\/j.apal.2026.103768_br0280","unstructured":"F.E. Miranda-Perea, E. Ugalde-Reyes, Minimal propositional logic strongly normalizes: A conciliating short mechanization in Rocq, unpublished manuscript, in preparation, 2025."},{"key":"10.1016\/j.apal.2026.103768_br0290","doi-asserted-by":"crossref","first-page":"569","DOI":"10.1023\/A:1021264102972","article-title":"Varieties of linear calculi","volume":"31","author":"Negri","year":"2002","journal-title":"J. Philos. Log."},{"key":"10.1016\/j.apal.2026.103768_br0300","series-title":"Structural Proof Theory","author":"Negri","year":"2001"},{"key":"10.1016\/j.apal.2026.103768_br0310","series-title":"Proof Analysis: A Contribution to Hilbert's Last Problem","author":"Negri","year":"2011"},{"key":"10.1016\/j.apal.2026.103768_br0320","author":"Nipkow"},{"key":"10.1016\/j.apal.2026.103768_br0330","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1007\/s001530100091","article-title":"Natural deduction with general elimination rules","volume":"40","author":"von Plato","year":"2001","journal-title":"Arch. Math. Log."},{"key":"10.1016\/j.apal.2026.103768_br0340","series-title":"Elements of Logical Reasoning","author":"von Plato","year":"2013"},{"key":"10.1016\/j.apal.2026.103768_br0350","series-title":"Gentzen's Centenary: The Quest for Consistency","first-page":"89","article-title":"From hauptsatz to hilfssatz","author":"von Plato","year":"2015"},{"key":"10.1016\/j.apal.2026.103768_br0360","series-title":"Advances in Proof-Theoretic Semantics","first-page":"139","article-title":"Explicit composition and its application in proofs of normalization","volume":"vol. 43","author":"von Plato","year":"2016"},{"key":"10.1016\/j.apal.2026.103768_br0370","doi-asserted-by":"crossref","first-page":"240","DOI":"10.2178\/bsl\/1208442829","article-title":"Gentzen's proof of normalization for natural deduction","volume":"14","author":"von Plato","year":"2008","journal-title":"Bull. Symb. Log."},{"key":"10.1016\/j.apal.2026.103768_br0380","series-title":"Natural Deduction: A Proof-Theoretical Study","author":"Prawitz","year":"1965"},{"key":"10.1016\/j.apal.2026.103768_br0390","series-title":"Proceedings of the Second Scandinavian Logic Symposium. Elsevier","first-page":"235","article-title":"Ideas and results in proof theory","volume":"vol. 63","author":"Prawitz","year":"1971"},{"key":"10.1016\/j.apal.2026.103768_br0400","series-title":"Intellectics and Computational Logic. Springer.","first-page":"453","article-title":"Proof = guarantee + explanation","volume":"vol. 19","author":"Robinson","year":"1980"},{"key":"10.1016\/j.apal.2026.103768_br0410","article-title":"Implicit epistemic aspects of constructive logic","volume":"191\u2013212doi","author":"Sundholm","year":"1997","journal-title":"J. Log. Lang. Inf."},{"key":"10.1016\/j.apal.2026.103768_br0420","series-title":"Lectures on the Curry-Howard Isomorphism","author":"S\u00f8rensen","year":"2006"},{"key":"10.1016\/j.apal.2026.103768_br0430","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","article-title":"Intensional interpretations of functionals of finite type I","volume":"32","author":"Tait","year":"1967","journal-title":"J. Symb. Log."},{"key":"10.1016\/j.apal.2026.103768_br0440","series-title":"Essays in Structural Proof Theory","author":"Tesconi","year":"2013"},{"key":"10.1016\/j.apal.2026.103768_br0450","article-title":"Constructivism in Mathematics: An Introduction (Volume I)","volume":"vol. 1","author":"Troelstra","year":"1988"},{"key":"10.1016\/j.apal.2026.103768_br0460","series-title":"Basic Proof Theory","author":"Troelstra","year":"2000"},{"key":"10.1016\/j.apal.2026.103768_br0470","series-title":"Principia Mathematica","volume":"vol. 1","author":"Whitehead","year":"1910"}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007226000515?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007226000515?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T08:52:18Z","timestamp":1780563138000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0168007226000515"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,10]]},"references-count":47,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2026,10]]}},"alternative-id":["S0168007226000515"],"URL":"https:\/\/doi.org\/10.1016\/j.apal.2026.103768","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[2026,10]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Mind the gap: A conciliating short proof of strong normalization for minimal propositional logic","name":"articletitle","label":"Article Title"},{"value":"Annals of Pure and Applied Logic","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.apal.2026.103768","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 The Authors. Published by Elsevier B.V.","name":"copyright","label":"Copyright"}],"article-number":"103768"}}