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.

Notwithstanding the advancements of formal methods, which already permit their adoption in a industrial context (consider, for instance, the notorious examples of Airbus, Amazon Web-Services, Facebook, or Intel), there is still no widespread endorsement. Namely, in the Portuguese case, it is seldom the case companies use them consistently, systematically, or both. One possible reason is the still low emphasis placed by academic institutions on formal methods (broadly consider as developments methodologies, verification, and tests), making their use a challenge for the current practitioners.

Formal methods build on logics, “the calculus of Computer Science”. Computational Logic is thus an essential field of Computer Science. Courses on this subject are usually either too informal (only providing pseudo-code specifications) or too formal (only pre- senting rigorous mathematical definitions) when describing algorithms. In either case, there is an emphasis on paper-and-pencil definitions and proofs rather than on computational approaches. It is scarcely the case where these courses provide executable code, even if the pedagogical advantages of using tools is well know.

In this dissertation, we present an approach to develop formally verified implementations of classical Computational Logic algorithms. We choose the Why3 platform as it allows one to implement functions with very similar characteristics to the mathematical definitions, as well as it concedes a high degree of automation in the verification process. As proofs of concept, we implement and show correct the conversion algorithms from propositional formulae to conjunctive normal form and from this form to Horn clauses.

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 and fundamental topics in Com- puter Science. Due to their rigorous and formal characteristics, learning these becomes demanding. An important support for the assimilation of concepts is the possibility of interactively visualizing concrete examples of these computational models, thus facilitat- ing their understanding. There are many tools available, but most are not complete or do not fully support the interactive aspect.

This project aims at the development of an interactive web tool in Portuguese to help understand, in an assisted and intuitive way, the concepts and algorithms in question, watching them work step-by-step, through typical examples pre-loaded or built by the user (an original aspect of our platform). The tool should therefore enable the creation and edition of an automaton or a regular expression, as well as execute the relevant classical algorithms such as word acceptance, model conversions, etc. Another important feature is that the tool has a clean design, in which everything is well organized and it is also extensible so that new features can be easily added later.

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 perfectly suitable 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 introduces the development of the tool, its design aspects that enable showing different conversions and processes as well as the development of the several functionalities related to the mechanisms already presented.

Due to its fairly formal nature, the teaching of the subject of Computation Theory often presents itself as a major obstacle for Computer Science students in general. To combat this, there have been developed many tools for the teaching of Formal Languages and Automata Theory (FLAT). Despite the considerable number of them, occasionally a new tool emerges that contributes with something new.

It was with this objective that we developed a library of OCaml functions that support various concepts of FLAT, namely the definition of finite automata, regular expressions and context-free grammars. Our implementation of these concepts closely follows their classical formalisation. We chose to implement this project using the OCaml language as it would allow us to write code according to the functional programming paradigm, which would better help us reach our defined goals.

In this report, to better contextualize the reader on the challenges and results of our project, we start by giving an overview of the properties of functional languages. Next, we give a small introduction to the FLAT concepts and discuss issues about their implementation. We then review the existing FLAT pedagogical tools.

After establishing our knowledge base, we discuss the architecture of our program. Next, we discuss the various FLAT algorithms and operations we implemented in our pro- gram, giving detailed insight on the decisions behind our implementations, as well as on solutions we found for the various technical difficulties such as guaranteeing termination of our algorithms, dealing with the nondeterminism of many concepts and catering to an extensible design. For our last topic, we discuss the top-level functionalities provided in our program.

We conclude that the usage of the functional programming paradigm, in combination with our adherence to the specified formalisms, allowed us to program our tool in a manner that made it viable for use in courses that teach FLAT concepts according to the classical definitions.

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.

Given the mathematical and formal character of the topics covered in subjects such as Languages and Automata, its teaching and learning processes are demanding and challenging. Several studies have confirmed these difficulties and evaluated the use of some applications. It is important to support students’ autonomous work with interactive tools that allow them to experiment with examples and solve exercise. There are a lot of applications that aim to overcome the difficulties mentioned by using various solutions. While some are quite complete, they are Desktop applications and not available everywhere. Others can be used via a web browser, although they are underdeveloped. The objective of this project is to develop an application serving as an experimental lab on Formal Languages and Automata Theory, FLAT, available through a browser. The idea is to create a tool that represents and animates graphically classical mechanisms and algorithms. It is also intended that this tool should be adapted to the course of Computational Theory taught at NOVA School of Science and Technology and that it includes not only exercises evaluated automatically and providing feedback, but also allowing students to create their own exercises. The application is being developed in Ocsigen Framework, which allows the creation of web application written in OCaml. By capitalizing of the features of OCaml, it is possible to obtain fully functional and less error-prone web pages. Ocsigen also facilitates the creation of web tools, as it allows to write client-side and server-side code in the same source file using the same language, thus facilitating system programming.