Related papers: Formalization of closure properties for context-fr…

We formalized general (i.e., type-0) grammars using the Lean 3 proof assistant. We defined basic notions of rewrite rules and of words derived by a grammar, and used grammars to show closure of the class of type-0 languages under four…

We present a Coq formalization of the Quantified Reflection Calculus with one modality, or $\mathsf{QRC}_1$. This is a decidable, strictly positive, and quantified modal logic previously studied for its applications in proof theory. The…

Large language models (LLMs) show remarkable promise for democratizing automated reasoning by generating formal specifications. However, a fundamental tension exists: LLMs are probabilistic, while formal verification demands deterministic…

We consider the cyclic closure of a language, and its generalisation to the operators $C^k$ introduced by Brandst\"adt. We prove that the cyclic closure of an indexed language is indexed, and that if $L$ is a context-free language then…

This work is a survey of the main results reported for the degree of extension of two models defining non-regular languages, namely the context-free grammar and the extended automaton over groups. More precisely, we recall the main results…

Formal deductive systems are very common in computer science. They are used to represent logics, programming languages, and security systems. Moreover, writing programs that manipulate them and that reason about them is important and…

In this paper we prove several results on normal forms for linear displacement context-free grammars. The results themselves are rather simple and use well-known techniques, but they are extensively used in more complex constructions.…

In this article we present a method for formally proving the correctness of the lazy algorithms for computing homographic and quadratic transformations -- of which field operations are special cases-- on a representation of real numbers by…

Context is a rich concept and is an elusive concept to define. The concept of context has been studied by philosophers, linguists, psychologists, and recently by computer scientists. Within each research community the term context was…

Whereas proof assistants based on Higher-Order Logic benefit from external solvers' automation, those based on Type Theory resist automation and thus require more expertise. Indeed, the latter use a more expressive logic which is further…

We develop a shape analysis for reasoning about relational properties of data structures. Both the concrete and the abstract domain are represented by hypergraphs. The analysis is parameterized by user-supplied indexed graph grammars to…

The introduction of first-class type classes in the Coq system calls for re-examination of the basic interfaces used for mathematical formalization in type theory. We present a new set of type classes for mathematics and take full advantage…

We give a natural complete infinitary axiomatization of the equational theory of the context-free languages, answering a question of Lei{\ss} (1992).

Proof assistants are getting more widespread use in research and industry to provide certified and independently checkable guarantees about theories, designs, systems and implementations. However, proof assistant implementations themselves…

Due to their numerous advantages, formal proofs and proof assistants, such as Coq, are becoming increasingly popular. However, one disadvantage of using proof assistants is that the resulting proofs can sometimes be hard to read and…

A number of flexible tactic-based logical frameworks are nowadays available that can implement a wide range of mathematical theories using a common higher-order metalanguage. Used as proof assistants, one of the advantages of such powerful…

In this paper we give a preliminary formalization of the p-adic numbers, in the context of the second author's univalent foundations program. We also provide the corresponding code verifying the construction in the proof assistant Coq.…

Classifying formal languages according to the expressiveness of grammars able to generate them is a fundamental problem in computational linguistics and, therefore, in the theory of computation. Furthermore, such kind of analysis can give…

We introduce a normal form for context-free grammars, called Dyck normal form. This is a syntactical restriction of the Chomsky normal form, in which the two nonterminals occurring on the right-hand side of a rule are paired nonterminals.…

We explore the application of transformer-based language models to automated theorem proving. This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans -- the generation of original…