Related papers: Infinite Words and Morphic Languages Formalized in…
An infinite word is an infinite Lyndon word if it is smaller, with respect to the lexicographic order, than all its proper suffixes, or equivalently if it has infinitely many finite Lyndon words as prefixes. A characterization of binary…
A logic for specification and verification is derived from the axioms of Zermelo-Fraenkel set theory. The proofs are performed using the proof assistant Isabelle. Isabelle is generic, supporting several different logics. Isabelle has the…
Given an infinite word X over an alphabet A a letter b occurring in X, and a total order \sigma on A, we call the smallest word with respect to \sigma starting with b in the shift orbit closure of X an extremal word of X. In this paper we…
We investigate the properties of formal languages expressible in terms of formulas over quantifier-free theories of word equations, arithmetic over length constraints, and language membership predicates for the classes of regular, visibly…
This report describes three particular technological advances in formal proofs. The HOL Light proof assistant will be used to illustrate the design of a highly reliable system. Today, proof assistants can verify large bodies of advanced…
An infinite permutation $\alpha$ is a linear ordering of $\mathbb N$. We study properties of infinite permutations analogous to those of infinite words, and show some resemblances and some differences between permutations and words. In this…
LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as proofs of correctness of decision procedures for LF's…
The main operations in Inductive Logic Programming (ILP) are generalization and specialization, which only make sense in a generality order. In ILP, the three most important generality orders are subsumption, implication and implication…
LTL3 is a multi-valued variant of Linear-time Temporal Logic for runtime verification applications. The semantic descriptions of LTL3 in previous work are given only in terms of the relationship to conventional LTL. Our approach, by…
Mission-time Linear Temporal Logic (MLTL) is rapidly increasing in popularity as a specification logic, e.g., for runtime verification and model checking, driving a need for a trustworthy tool base for analyzing MLTL. In this work, we…
We have previously published the Isabelle/HOL formalization of a general theory of syntax with bindings. In this companion paper, we instantiate the general theory to the syntax of lambda-calculus and formalize the development leading to…
We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the first-order logic of real arithmetic to a logically…
We consider the problem of how to verify the security of probabilistic oblivious algorithms formally and systematically. Unfortunately, prior program logics fail to support a number of complexities that feature in the semantics and…
Existential rules are an expressive knowledge representation language mainly developed to query data. In the literature, they are often supposed to be in some normal form that simplifies technical developments. For instance, a common…
In this book chapter, written in French, we consider the classical family of Sturmian words, defined as the aperiodic infinite words containing only $n+1$ factors of a length $n$, which is the minimal possible value. We will discuss several…
We make a systematic study of the infinitesimal lifting conditions of a pseudo finite type map of noetherian formal schemes. We recover the usual general properties in this context, and, more importantly, we uncover some new phenomena. We…
This work is a mathematician's attempt to understand intuitionistic logic. It can be read in two ways: as a research paper interspersed with lengthy digressions into rethinking of standard material; or as an elementary (but highly…
We introduce a topological approach to words. Words are approximated by Gauss words and then studied up to natural modifications inspired by homotopy transformations of curves on the plane.
Education in the practical applications of logic and proving such as the formal specification and verification of computer programs is substantially hampered by the fact that most time and effort that is invested in proving is actually…
Autoformalization, the process of transforming informal mathematical propositions into verifiable formal representations, is a foundational task in automated theorem proving, offering a new perspective on the use of mathematics in both…