## Animated Logic: Correct Functional Conversion to Conjunctive Normal Form

×

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.

## Formally Verified Bug-free Implementations of (Logical) Algorithms

×

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.

## Visualização e animação de autómatos em Ocsigen Framework

×

## OCaml-FLAT on the Ocsigen Framework

×

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.

## OCaml-Flat - An OCaml Toolkit for experimenting with formal languages theory

×

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.

## Defuncionalize to proof

×

## Functional Programming with style and costless: CPS transformation "à la carte"

×

## A mechanized proof of correctness of the Hornalgorithm

×

## Rewinding functions through CPS

×

## Publications

### Computational Logic

- Animated Logic I: Correct Functional Conversion to Conjunctive Normal Form - Pedro Barroso, Mário Pereira and António Ravara - [Abstract] - [English Version] - [Portuguese Version] - Presented at INForum 2019 - Computer Symposium
- Formally Verified Bug-free Implementations of (Logical) Algorithms - Pedro Barroso - [Abstract] - [pdf]
- Defunctionalize to prove [text in Portuguese] - Mário Pereira - [Abstract] - [pdf]

### Formal Languages & Automata Theory

- Visualization and Animation of Automata on Ocsigen Framework [text in Portuguese] - Rita Macedo, Artur Miguel Dias, António Ravara - [Abstract] - [Extended Abstract] - [pdf] - Presented at INForum 2019 - Computer Symposium
- OCaml-Flat on the Ocsigen Framework (report to support the intermediate evaluation of the dissertation) [text in Portuguese] - Rita Macedo - [Abstract] - [pdf]
- OCaml-Flat - An OCaml Toolkit for experimenting with formal languages theory (report to support the intermediate evaluation of the dissertation) - João Gonçalves - [Abstract] - [pdf]

### Advanced Programming

- A mechanized proof of correctness of the Horn algorithm - Marco Giunti - [Background] - [pdf]
- Compiling linear and static channels in Go - Marco Giunti - [pdf]
- Rewinding functions through CPS - Marco Giunti - [Background] - [pdf]
- Functional Programming with style and costless: CPS transformation "à la carte" [text in Portuguese] - Tiago Roxo, Mário Pereira, and Simão Melo de Sousa - [Abstract] - [pdf]