We present an approach to obtain formally verified implementations of classical ComputationalLogic algorithms. We choose the Why3 platform because it allows to implement functions in a stylevery close to the mathematical definitions, as well as it allows a high degree of automation in theverification process.

As proof of concept, we present a mathematical definition of the algorithm to convert propositional formulae to conjunctive normal form, implementations in WhyML (the Why3 language, very similarto OCaml), and proofs of correctness of the implementations. We apply our proposal on two variantsof this algorithm: one in direct-style and another with an explicit stack structure. Being bothfirst-order versions, Why3 processes the proofs naturally.

Computational Logic is an essential field of Computer Science. Courses on this subject are either too informal (only providing pseudo-codes) or too formal when describing algorithms. In either case, there is an emphasis on paper-and-pencil proofs rather than on computational approaches. It is seldom the case that there are running algorithms (executable programs). Implementations of algorithms and tools that help students go through the resolutions of exercises are crucial, as they are an important pedagogical object.

Most courses make only a small or no effort on showing the presented algorithms correction, although this is an important aspect of software development that should be natural for Computer Science students. For instance, the Integrated Master in Computer Science course of the Faculty of Science and Technology of NOVA University of Lisbon only starts referring to program verification in the 4th year. Students often make wrong assumptions over the correction of their programs basing themselves in tests, which are not enough to prove that a program is completely bug-free. Tests only discover the presence of bugs. To assure that a program is correct we must use formal verification instead.

The purpose of this dissertation is to contribute to the formalization and assisted- verification of standard and classical algorithms of Computational Logic, through the de- velopment of step-by-step implementations of those algorithms in a functional language (the nature of these languages offers a closer relationship to mathematical definitions) and posterior verification of such implementations using the Why3 program verification plat- form. These implementations and soundness proofs will serve as pedagogical material to Computational Logic students.

Formal Languages and Automata Theory are important foundational topics in Computer Science. Their rigorous and formal characteristics make their learning them demanding. An important support for the assimilation of concepts is the possibility of interactively visualizing concrete examples of these computational models, facilitating understanding them. The tools available are neither complete nor fully support the interactive aspect. This project aims at the development of an interactive web tool in Portuguese to help in an assisted and intuitive way to understand the concepts and algorithms in question, seeing them work step-by-step, through typical examples preloaded or built by the user (an original aspect of our platform). The tool should therefore enable the creation and edition of an automata, as well as execute the relevant classical algorithms such as word acceptance, model conversions, etc. It is also intended to visualize not only the process of construction of the automaton, but also all the steps of applying the given algorithm. This tool uses the Ocsigen Framework because it provides the development of complete and interactive web tools written in OCaml, a functional language with a strong type checking system and therefore perfect for a web page without errors. Ocsigen was also chosen because it allows the creation of dynamic pages with a singular client-server system. This article presents the first phase of the development of the project. It is already possible to create automata, check the nature of its states and verify step-by-step (with undo) the acceptance of a word.

Formal Languages and Automata Theory are important foundational topics in Computer Science. Their rigorous and formal characteristics makelearning them demanding. An important support for the assimilation of concepts is the possibility of interactively visualizing concrete examples of these computational models, facilitating understanding them. The tools available are neither complete nor fully support the interactive aspect.

his project aims at the development of an interactive web tool in Portuguese to help in an assisted and intuitive way to understand the concepts and algorithms in question, seeing them work step-by-step, through typical examples preloaded or built by the user (an original aspect of our platform). The tool should therefore enable the creation and edition of an automata, as well as execute the relevant classical algorithms such as word acceptance, model conversions, etc. It is also intended to visualize not only the process of construction of the automaton, but also all the steps of applying the given algorithm.

This tool uses the Ocsigen Framework because it provides the development of complete and interactive web tools written in OCaml, a functional language with a strong type checking system and therefore perfect for a web page without errors. Ocsigen was also chosen because it allows the creation of dynamic pages with a singular client-server system.

This document presents de project proposal and the first phase of it’s development. It is already possible to create automata, check the nature of its states and verify step-bystep (with undo) the acceptance of a word.

Due to its fairly formal nature, the teaching of the subject of computation theory often presents itself as a major obstacle for computer students in general. The academic community has for some time been aware of this situation. Historically there have been developed many tools for the teaching of theory of formal languages and automata (FLAT).

Despite the existence of a considerable number of them, occasionally a new tool emerges that contributes with something new, or some existing tools are extended with new functionalities.

We propose to develop a library of functions in OCaml that support various concepts of FLAT, namely the definition of finite automata, regular expressions, pushdown automata, context-free grammars and Turing machines. We want to provide code that, whenever possible, follows closely the formalization of the concepts studied by the students.

Another goal is to provide support for using this system inside Mooshak.

Finally, an interesting technical problem we will need to handle is the nondeterminism and nontermination in parts of the code.

In this report, first we discuss the properties of functional languages and why they are indicated for our project. Next, we give a small introduction to the FLAT concepts and discuss some issues about their implementation. Finally, there is a small review on the existing FLAT pedagogical tools.

This paper explores the idea of using defunctionalization as a proof technique for higher-order programs. Defunctionalization builds on substituting functional values by a first-order representation. Thus, its interest is that one can use an existing program verification tool, without further extensions in order to support higher-order. This papers illustrates and discusses this approach by means of several running examples, built and verified using the Why3 verification framework.

In this paper we explore the use of CPS as an automatic program transformation. CPS is a programming style that allows one to convert any non-tail recursive function into a terminal recursive one, using constant stack space. Hence, Stack Overflow problems are eliminated by construction, assuming the underlying compiler is able to optimize tail-recursive implementations. The code transformation phase is done via an OCaml syntactic extension, called a PPX. In this paper, we describe how we automate the CPS transformation mechanism, how it is transparently integrated into the compilation scheme, and we assess perform differences between CPS and direct implementations.

This abstract presents a mechanized proof of correctness of a variant [4] of the Horn algorithm in the automated prover Why3 [2]. The paper [4] introduces a functional presentation of the Horn algorithm [3] that is based on a recursive formulation. This is in contrast with the usual pseudo-code imperative presentations of the Horn algorithm, and allows 1) a concise, yet rigorous, formalisation; 2) a clear form of visualising executions of the algorithm, step-by- step; 3) precise results, simple to state and with clean inductive proofs. Roughly, the algorithm receives a conjunction of Horn clauses presented as implications of the form A ! B, and recursively accumulates a set of symbols B1; : : : ;Bn by inspecting if A1; : : : ;An are contained in the dynamically built set. The procedure ends when a xpoint is reached, that is the next iteration does not change the accumulator, and returns 1 whenever ? is not in the set, and 0 otherwise. The paper proves that the algorithm is sound and complete: the result is 1 if and only if the formula is satisable, and the result is 0 if and only if the formula is contradictory.

The ability to rewind or step back computations is fundamental in many functional programming approaches, which include the teaching of foundational computing courses, by allowing step-wise execution of algorithms, and the debugging of functional applications, by permitting the inspection of the intermediate values of recursive computations. In this report, we present a functional programming pearl that shows how this can be accomplished in continuation-passing style (CPS) by tracing the argument and the continuation of each recursive call. To obtain maximum generality, the mechanism is provided by means of a monad transformer that adds trace functionalities to arbitrary monads. We show applications of the transformation involving algebraic types, data structures, references, and exceptions, and conclude by presenting a functor that provides support for the automatic generation of CPS functions with rewind functionalities.