Este projeto visa promover o uso do OCaml na comunidade académica de expressão portuguesa, nomeadamente através do apoio a abordagens e ferramentas de ensino. Em particular, visa ampliar e consolidar a base de utilizadores de software e materiais de ensino em OCaml na língua portuguesa para disciplinas na área de Lógica Computacional e Fundamentos de Computação em cursos de Informática.
O projeto é formalmente gerido pelo DI da UBI, mas insere-se no centro de investigação NOVA LINCS. O responsável pelo projeto é o Prof. Simão Melo de Sousa, sendo os restantes membros o Prof. António Ravara e o Prof. Artur Miguel Dias.
O projeto é financiado pela Tezos Foundation, que suporta bolsas para alunos da UBI e da FCT/UNL que estejam a iniciar o trabalho das dissertações de Mestrado. [Google: tezos ocaml]
(24/out/2018)
As bolsas têm um valor superior ao normal, cerca de 850€/mês (em vez de 745€), ao longo de nove meses.
Soundness is presently a major challenge for programmers - the societal tolerance to software bugs and hacker infiltrations is decreasing rapidly, with prominent cases making shocking news almost daily. Surprisingly, there are effective methodologies and tools to ensure strong guarantees about the safety and the reliability of programs, as witnessed by several successful industrial cases:
The vast majority of developers, however, have little training in developing bug-free and hacker-proofed program. Moreover, most companies lack the know-how and practices to deal with these software soundness challenges. The challenging is at the same time huge and urgent. This thesis proposal is a (quite) small step to face it.
The aim of this project is to develop formally verified functional implementations of classical logical algorithms like the Horn satisfiability. Concretely, the objective is twofold: - the functional implementation of classical logical algorithms as showcases of clean and clear code close to specifications; - the development of correctness proofs of the implementations as showcases of the feasibility and usability of machine-checked program proof systems.
Formal languages and automata theory (FLAT) is a core subject in Computer Science, but the formal nature of the matter constitutes a difficulty to many students. It helps to have an interactive environment supporting the definition and testing of language generators and language recognizers. The programming language OCaml is a natural candidate to the implementation of such environment: it is a very clean and elegant language supporting the functional paradigm and with strong symbolic processing abilities.
This MSc Dissertation proposal aims at promoting the use of OCaml in the Portuguese speaking academic community, namely by providing support to teaching approaches and tools. In particular, it aims at extending and consolidating the OCaml software user base and teaching materials in the Portuguese language for Computational Logic and Foundation of Computing courses in undergraduate Computer Science degrees.
The MSc student is expected to develop a FLAT toolkit to support the definition of alphabets, order relations and languages. The languages will be mainly defined using language generators and language recognizers. Here are some definitional mechanisms to support: predicates (Boolean functions), regular expressions, finite automata, context-free grammars, push-down automata, Turing machines.
Conversion between mechanisms would also be interesting, for examples rewriting a regular expression in the form of a context-free grammar.
It should also be possible to check a language definition against a set of unit test, to support the integration of the system in an automatic programming evaluation system (such as Mooshak, or other).
Avoiding endless loops will be a concern in the implementation of the nondeterministic definitional mechanisms. It will be necessary to explore all the alternatives in parallel and use a mechanism for detection of repeated configurations.
Formal languages and automata theory (FLAT) is a core subject in Computer Science, but the formal nature of the matter constitutes a difficulty to many students. It helps to have an interactive environment supporting the definition and testing of language generators and language recognizers. The programming language OCaml is a natural candidate to the implementation of such environment: it is a very clean and elegant language supporting the functional paradigm and with strong symbolic processing abilities.
This MSc Dissertation proposal aims at promoting the use of OCaml in the Portuguese speaking academic community, namely by providing support to teaching approaches and tools. In particular, it aims at extending and consolidating the OCaml software user base and teaching materials in the Portuguese language for Computational Logic and Foundation of Computing courses in undergraduate Computer Science degrees.
The MSc student is expected to develop a graphical interface for OCaml-Flat using the Ocsigen framework. Other similar systems, such as JFLAP, should be studied. The main general functionalities:
It is assumed that, at least the components of OCaml-Flat concerning regular expressions and finite automata are already available. Some care should be taken, so that the approach is adaptable to other mechanisms.
Probably, half of the effort of this project will consist in gaining in-depth knowledge of the Ocsigen framework and how to create graphical rich interactive Web pages using the framework.
Formal languages and automata theory (FLAT) is a core subject in Computer Science, but the formal nature of the matter constitutes a difficulty to many students. It helps to have an interactive environment supporting the definition and testing of language generators and language recognizers. The programming language OCaml is a natural candidate to the implementation of such environment: it is a very clean and elegant language supporting the functional paradigm and with strong symbolic processing abilities.
This thesis will expand on work currently being finished around two software tools: (1) OCaml-FLAT, a sophisticated OCaml library that supports many concepts of FLAT, and (2) OFLAT, an interactive Web application for FLAT concepts, developed on top of OCaml-FLAT with the help of the Ocsigen framework (which is fully programmable in OCaml). These tools already gained some degree of maturity, but there are many improvements to be made, new funcionalities to be added, also adaptations to new contexts.
The main goal is to adapt and to integrate OFLAT in the Learn-OCaml platform (http://ocaml.hackojo.org/). The original version of OFLAT has been developed within the Ocsigen framework and Learn-OCaml is quite different. Learn OCaml is a fully featured platform for learning the OCaml language that supports registered users, exercises, quizzes, etc. We want to capitalize on that infrastructure and also, in return, to make available our tools to the Learn-OCaml community. It will be necessary to study the arquitecture of Learn-OCaml.
The second goal is to make OFLAT multilingual, by adding some internationalization mechanism (i18n).
The third and final goal consists in extending OCaml-FLAT and OFLAT to support pushdown automata and LL(1) grammars.
In this thesis, the general goal is to eliminate some of the roadblocks that hinder the use of an declarative style in OCaml. This will be achieved by developing tools and techniques for the generation of efficient code from purely declarative OCaml programs. From an executional perspective, declarative definitions are usually less efficient when compared to more machine-friendly solutions. One typical example is that of tail-recursive recursive definitions. Even if we all appreciate the benefits of this approach, we believe that more direct implementations still worth to be considered.
Here are the main research lines to be pursued:
1 - Investigate and implement automatic transformations to convert purely declarative OCaml programs into equivalent intermediate representations, which are more suitable for producing efficient code. Develop a PPX (PreProcessor eXtensions), taking a parsed tree from the OCaml compiler and automatically convert it to a new, equivalent tree to produce more efficient code. Previous work presented a PPX to convert recursive definitions into CPS-equivalent definitions, automatically eliminating all Stack Overflow problems from the original code.
2 - Dig into a very specific part of the OCaml compiler and propose a different compilation scheme for declarative programs.
3 - Explore the use of automatic memoing as another way to manage the execution time of declarative code. Note that this technique can even transform exponential execution times into linear execution times - the trade-off is extra memory consumption.