Related papers: A simple formalization of alpha-equivalence
The logical technique of focusing can be applied to the $\lambda$-calculus; in a simple type system with atomic types and negative type formers (functions, products, the unit type), its normal forms coincide with $\beta\eta$-normal forms.…
We provide a computational definition of the notions of vector space and bilinear functions. We use this result to introduce a minimal language combining higher-order computation and linear algebra. This language extends the Lambda-calculus…
We present a prototype of an integrated reasoning environment for educational purposes. The presented tool is a fragment of a proof assistant and automated theorem prover. We describe the existing and planned functionality of the theorem…
Scientific computing programs often undergo aggressive compiler optimization to achieve high performance and efficient resource utilization. While performance is critical, we also need to ensure that these optimizations are correct. In this…
The Abella interactive theorem prover has proven to be an effective vehicle for reasoning about relational specifications. However, the system has a limitation that arises from the fact that it is based on a simply typed logic:…
We study the structure of the partial order induced by the definability relation on definitions of truth for the language of arithmetic. Formally, a definition of truth is any sentence $\alpha$ which extends a weak arithmetical theory…
We present a new lambda-calculus with explicit substitutions and named variables. Renaming of bound variables in this calculus is explicit (there is a special rewrite rule) and can be delayed. Contexts (environments) are not sets or lists…
We exploit (co)inductive specifications and proofs to approach the evaluation of low-level programs for the Unlimited Register Machine (URM) within the Coq system, a proof assistant based on the Calculus of (Co)Inductive Constructions type…
In this position paper, we would like to offer and defend a new template to study equivalences between programs -- in the particular framework of process algebras for concurrent computation.We believe that our layered model of development…
Formulating a Schubert problem as the solutions to a system of equations in either Pl\"ucker space or in the local coordinates of a Schubert cell usually involves more equations than variables. Using reduction to the diagonal, we previously…
Integration, just as much as differentiation, is a fundamental calculus tool that is widely used in many scientific domains. Formalizing the mathematical concept of integration and the associated results in a formal proof assistant helps in…
Initial Semantics aims at characterizing the syntax associated to a signature as the initial object of some category. We present an initial semantics result for typed higher-order syntax together with its formalization in the Coq proof…
The need for formal definition of the very basis of mathematics arose in the last century. The scale and complexity of mathematics, along with discovered paradoxes, revealed the danger of accumulating errors across theories. Although,…
Context-free language theory is a well-established area of mathematics, relevant to computer science foundations and technology. This paper presents the preliminary results of an ongoing formalization project using context-free grammars and…
We describe a formalization of higher-order rewriting theory and formally prove that an AFS is strongly normalizing if it can be interpreted in a well-founded domain. To do so, we use Coq, which is a proof assistant based on dependent type…
We introduce a linear infinitary $\lambda$-calculus, called $\ell\Lambda_{\infty}$, in which two exponential modalities are available, the first one being the usual, finitary one, the other being the only construct interpreted…
Open-domain question answering (Open-QA) is a common task for evaluating large language models (LLMs). However, current Open-QA evaluations are criticized for the ambiguity in questions and the lack of semantic understanding in evaluators.…
We present a sequent calculus for abstract focussing, equipped with proof-terms: in the tradition of Zeilberger's work, logical connectives and their introduction rules are left as a parameter of the system, which collapses the synchronous…
Reynold's parametricity theory captures the property that parametrically polymorphic functions behave uniformly: they produce related results on related instantiations. In dependently-typed programming languages, such relations and…
Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in functional frameworks are surveyed in the…