Related papers: Maths with Coq in L1, a pedagogical experiment
Physics lab courses are integral parts of an undergraduate physics education, and offer a variety of opportunities for learning. Many of these opportunities center around a common learning goal in introductory physics lab courses:…
This paper presents a Coq formalization of linear algebra over elementary divisor rings, that is, rings where every matrix is equivalent to a matrix in Smith normal form. The main results are the formalization that these rings support…
The present article is an empirical study that investigates the learning situation of linear algebra. Research was performed among 60 science and engineering students from different universities in Zhejiang, Jiangsu, Hubei, and Shandong who…
Should the final right bracket in a record declaration be on a separate line? Should arguments to the rewrite tactic be separated by a single space? Coq code tends to be written in distinct manners by different people and teams. The…
The study, conducted over a four-year academic cycle with the assistance of M2 students from the Cyberjustice Master's programme at the Faculty of Law, Political Science and Management at the University of Strasbourg, aims to objectively…
Creating safe concurrent algorithms is challenging and error-prone. For this reason, a formal verification framework is necessary especially when those concurrent algorithms are used in safety-critical systems. The goal of this guide is to…
We present the Sequent Calculus Trainer, a tool that supports students in learning how to correctly construct proofs in the sequent calculus for first-order logic with equality. It is a proof assistant fostering the understanding of all the…
Significant obstacles prevent large, university-level, introductory physics courses from effectively teaching problem-solving skills. We describe our program for integrating three internet-based "teaching-while-quizzing" tools to address…
This paper presents experiments on common knowledge logic, conducted with the help of the proof assistant Coq. The main feature of common knowledge logic is the eponymous modality that says that a group of agents shares a knowledge about a…
Proof search in non-confluent tableau calculi, such as the connection tableau calculus, suffers from excess backtracking, but simple restrictions on backtracking are incomplete. We adopt constraint learning to reduce backtracking in the…
In this work, we develop statistical tools to understand core courses at the university level. Traditionally, professors and administrators label courses as "core" when the courses contain foundational material. Such courses are often…
Several approaches exist to data-mining big corpora of formal proofs. Some of these approaches are based on statistical machine learning, and some -- on theory exploration. However, most are developed for either untyped or simply-typed…
Theory of Computing (ToC) is an important course in CS curricula because of its connections to other CS courses as a foundation for them. Traditional ToC course grading schemes are mostly exam-based, and sometimes a small weight for…
We report on using an agentic coding assistant (Claude Code, powered by Claude Opus 4.6) to mechanize a substantial Rocq correctness proof from scratch, with human guidance but without human proof writing. The proof establishes semantic…
Between 2017 and 2019, a standard Linear Algebra course from Instituto Superior T\'ecnico, University of Lisbon, used virtual learning content, mainly videos and formative assessment, delivered at the institution's MOOC platform to support…
The syntax of an imperative language does not mention explicitly the state, while its denotational semantics has to mention it. In this paper we present a framework for the verification in Coq of properties of programs manipulating the…
In this work, we investigate whether improving task clarity can enhance reasoning ability of large language models, focusing on theorem proving in Coq. We introduce a concept-level metric to evaluate task clarity and show that adding…
This paper documents our experience using declarative languages to give secondary school students a first taste of Computer Science. The course aims to teach students a bit about programming in Prolog, but also exposes them to important…
PyLog is a minimal experimental proof assistant based on linearised natural deduction for intuitionistic and classical first-order logic extended with a comprehension operator. PyLog is interesting as a tool to be used in conjunction with…
Proof assistants are software-based tools that are used in the mechanization of proof construction and validation in mathematics and computer science, and also in certified program development. Different tools are being increasingly used in…