Related papers: A Formalization of Operads in Coq
We present a formal model of Checked C, a dialect of C that aims to enforce spatial memory safety. Our model pays particular attention to the semantics of dynamically sized, potentially null-terminated arrays. We formalize this model in…
Fact verification based on structured data is challenging as it requires models to understand both natural language and symbolic operations performed over tables. Although pre-trained language models have demonstrated a strong capability in…
Type soundness is an important property of modern programming languages. In this paper we explore the idea that "well-typed languages are sound": the idea that the appropriate typing discipline over language specifications guarantees that…
Text editors represent one of the fundamental tools that writers use - software developers, book authors, mathematicians. A text editor must work as intended in that it should allow the users to do their job. We start by introducing a small…
The Coq Platform is a continuously developed distribution of the Coq proof assistant together with commonly used libraries, plugins, and external tools useful in Coq-based formal verification projects. The Coq Platform enables reproducing…
In this project, a rather complete proof-theoretical formalization of Lambek Calculus (non-associative with arbitrary extensions) has been ported from Coq proof assistent to HOL4 theorem prover, with some improvements and new theorems.…
We present an approach for representing abstract argumentation frameworks based on an encoding into classical higher-order logic. This provides a uniform framework for computer-assisted assessment of abstract argumentation frameworks using…
Programming language frameworks allow us to generate language tools (e.g., interpreters) just from a formal description of the syntax and semantics of a programming language. As these frameworks tend to be quite complex, an issue arises…
We argue that in some KR applications, we want to quantify over sets of concepts formally represented by symbols in the vocabulary. We show that this quantification should be distinguished from second-order quantification and…
Despite extensive research both on the theoretical and practical fronts, formalising, reasoning about, and implementing languages with variable binding is still a daunting endeavour - repetitive boilerplate and the overly complicated…
One of the effective model checking methods is to utilize the efficient decision procedure of SAT (or SMT) solvers. In a SAT-based model checking, a system and its property are encoded into a set of logic formulas and the safety is checked…
Program logics are a powerful formal method in the context of program verification. Can we develop a counterpart of program logics in the context of language verification? This paper proposes language logics, which allow for statements of…
Describing systems in terms of choices and their resulting costs and rewards offers the promise of freeing algorithm designers and programmers from specifying how those choices should be made; in implementations, the choices can be realized…
Dynamic evaluation is a paradigm in computer algebra which was introduced for computing with algebraic numbers. In linear algebra, for instance, dynamic evaluation can be used to apply programs which have been written for matrices with…
This paper proposes {\pi}, a formal semantic framework for compiler construction together with program validation. {\pi} is comprised by {\pi} Lib, a set of programming languages constructs inspired by Peter Mosses' Component-Based…
Most existing implementations of multiple precision arithmetic demand that the user sets the precision {\em a priori}. Some libraries are said adaptable in the sense that they dynamically change the precision of each intermediate operation…
Proof assistants enable users to develop machine-checked proofs regarding software-related properties. Unfortunately, the interactive nature of these proof assistants imposes most of the proof burden on the user, making formal verification…
We introduce Clerical, a programming language for exact real-number computation that combines first-order imperative-style programming with a limit operator for computation of real numbers as limits of Cauchy sequences. We address the…
Proof-oriented programming languages (POPLs) empower developers to write code alongside formal correctness proofs, providing formal guarantees that the code adheres to specified requirements. Despite their powerful capabilities, POPLs…
In this paper we focus on the development of a toolbox for the verification of programs in the context of SCOOP -- an elegant concurrency model, recently formalized based on Rewriting Logic (RL) and Maude. SCOOP is implemented in Eiffel and…