2026-07-22T02:02:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24635 2025-12-12T15:10:08Z ddc:004 open_access

LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper) Vin, Eric Miller, Kyle A. Fremont, Daniel J. Linear Temporal Logic Interactive Theorem Proving Lean 4 We propose LeanLTL, a unifying framework for linear temporal logics in Lean 4. LeanLTL supports reasoning about traces that represent either infinite or finite linear time. The library allows traditional LTL syntax to be combined with arbitrary Lean expressions, making it straightforward to define properties involving numerical or other types. We prove that standard flavors of LTL can be embedded in our framework. The library also provides automation for reasoning about LeanLTL formulas in a way that facilitates using Lean’s existing tactics. Finally, we provide examples illustrating the utility of the library in reasoning about systems that come from applications. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Eric Vin and Kyle A. Miller and Daniel J. Fremont 2025 Is Part Of LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2025.37 urn:nbn:de:0030-drops-246356 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.37 eng https://creativecommons.org/licenses/by/4.0/legalcode