## 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

×

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.

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

×

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.

## 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

×

## 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

- OCaml-Flat on the Ocsigen Framework Extended Abstract - Rita Macedo - [Abstract] - [pdf] - Presented at WiL 2020 - The 4th Women in Logic Workshop
- 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 - Rita Macedo - [Abstract] - [pdf]
- OCaml-Flat - An OCaml Toolkit for experimenting with formal languages theory - 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]