Related papers: Anatomy of a Formal Proof
Foundations of formal languages, as subfield of theoretical computer science, are part of typical upper secondary education curricula. There is very little research on the potential difficulties that students at this level have with this…
Many universities have courses and projects revolving around compiler or interpreter implementation as part of their degree programmes in computer science. In such teaching activities, tool support can be highly beneficial. While there are…
Mathematical understanding is built in many ways. Among these, illustration has been a companion and tool for research for as long as research has taken place. We use the term illustration to encompass any way one might bring a mathematical…
Interactive program verification is characterized by iterations of unfinished proof attempts. To support the process of constructing a complete proof, many interactive program verification systems offer a proof scripting language as a…
This comprehensive survey examines Lean 4, a state-of-the-art interactive theorem prover and functional programming language. We analyze its architectural design, type system, metaprogramming capabilities, and practical applications in…
We present the proof assistant homotopy.io for working with finitely-presented semistrict higher categories. The tool runs in the browser with a point-and-click interface, allowing direct manipulation of proof objects via a graphical…
Education in the practical applications of logic and proving such as the formal specification and verification of computer programs is substantially hampered by the fact that most time and effort that is invested in proving is actually…
Mathematical proofs are a cornerstone of control theory, and it is important to get them right. Deduction systems can help with this by mechanically checking the proofs. However, the structure and level of detail at which a proof is…
The use of logical systems for problem-solving may be as diverse as in proving theorems in mathematics or in figuring out how to meet up with a friend. In either case, the problem solving activity is captured by the search for an…
In recent years, program verifiers and interactive theorem provers have become more powerful and more suitable for verifying large programs or proofs. This has demonstrated the need for improving the user experience of these tools to…
This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for…
An invaluable feature of computer algebra systems is their ability to plot the graph of functions. Unfortunately, when one is trying to design a library of mathematical functions, this feature often falls short, producing incorrect and…
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…
Verification is one of the central tasks in circuit and system design. While simulation and emulation are widely used, complete correctness can only be ensured based on formal proof techniques. But these approaches often have very high run…
We offer a view of mathematics as an experimental science where axioms play the role of foundational theories like general relativity and quantum mechanics in physics. Under this view, axioms are provisional and inferred from experience…
Proof assistants like Coq are increasingly popular to help mathematicians carry out proofs of the results they conjecture. However, formal proofs remain highly technical and are especially difficult to reuse. In this paper, we present a…
In this work, we show a methodology aimed to improve the quality of the assessment process for subjects related to basic programming. The method takes into account the relevance of the items and the students answers to follow different…
The application of automatic theorem provers to discharge proof obligations is necessary to apply formal methods in an efficient manner. Tools supporting formal methods, such as Atelier~B, generate proof obligations fully automatically.…
In the theory of programming languages, type inference is the process of inferring the type of an expression automatically, often making use of information from the context in which the expression appears. Such mechanisms turn out to be…
We present an approach to program reasoning which inserts between a program and its verification conditions an additional layer, the denotation of the program expressed in a declarative form. The program is first translated into its…