We all know that we can use Haskell to write functional programs that compute stuff. But can we also use Haskell to write mathematical proofs? Yes!
This post is intended to be a guided exercise (with a proposed solution) for Agda beginner's who are familiar with the basics and want to work on a slightly more involved exercise than proving basic properties about natural numbers.
I present an Agda eDSL for writing Hilbert style proofs for logic $K$.
Sufficiently strong arithmetical theories such as PA can formalize their interpretability predicate. This predicate expresses the concept of relativized interpretability between finite extensions of the theory. Interpretability logics study the provable structural behaviour of the interpretability predicate. Interpretability logics extend the provability logic GL. As such, interpretability logics inherit a number of similarities from GL. For instance, the possibility to give relational semantics. In this thesis we focus on the study of two variations of relational semantics à la Kripke known as ordinary Veltman semantics and generalized Veltman semantics. In the literature we find various definitions of generalized Veltman semantics. In particular, there are several conditions of quasi-transitivity, a property that generalized frames must satisfy. We study the interrelations between all of these conditions and discuss their adequacy. In this thesis we compare the expressiveness of ordinary and generalized Veltman semantics. Furthermore, we give procedures that under some assumptions transform, while preserving modal theoremhood, ordinary models to generalized models and vice versa. We study the frame conditions of various relevant interpretability principles present in the literature. Moreover, we provide novel frame conditions for the the principle R1 and the Rn series of principles from  with respect to generalized Veltman semantics. We have formalized our findings in Agda, which is a state-of-the-art proof assistant based on an intuitionistic theory which features dependent types. Apart from giving a solid base to our claims, we hope that our Agda library will provide a rallying point for researchers willing to formalize theorems in the field of interpretability logics, or at least, to encourage more research in that direction. Our work is, to our knowledge, the first attempt at formalizing interpretability logics in any proof assistant.
In this extended abstract we compute some rather involved frame conditions w.r.t.Generalised Veltman Semantics for principles of interpretability logic. All proofs have been formalised in Agda and we briefly comment on this formalisation.
Interpretability logics are endowed with relational semantics `a la Kripke: Veltman semantics. For certain applications though, this semantics is not fine-grained enough. Back in 1992 the notion ofgeneralised Veltman semantics emerged to obtain certain non-derivability results as was first presented by Verbrugge. It has turned out that this semantics has various good properties. In particular, in many cases completeness proofs become simpler and the richer semantics will allow for filtration arguments as opposed to regular Veltman semantics. This paper aims to give an overview of results and applications of Generalised Veltman semantics up to the current date.
Jutge.org is an open educational online programming judge designed for students and instructors, featuring a repository of problems that is well organized by courses, topics, and difficulty. Internally, Jutge.org uses a secure and efficient architecture and integrates modern verification techniques, formal methods, static code analysis, and data mining. Jutge.org has exhaustively been used during the last decade at the Universitat Politècnica de Catalunya to strengthen the learning-by-doing approach in several courses. This paper presents the main characteristics of Jutge.org and shows its use and impact on a wide range of courses covering basic programming, data structures, algorithms, artificial intelligence, functional programming, and circuit design.
Computer Engineering, 2014
Polytechnic University of Catalonia
Master in Advanced Computing, 2017
Polytechnic University of Catalonia / Chalmers University of Technology
Master in Pure and Applied Logic, 2020
University of Barcelona