Propositional Dynamic Logic (PDL) [1] is a logic in which abstract properties about the behaviour of programs can be expressed, in a very general way. Because of its generality it is suitable for checking the behaviour or a wide range of programs and systems, via model checking. PDL is what is known as a modal … full description “A Cyclic Prover for Propositional Dynamic Logic (available)”
Supervisor: Reuben Rowe
Active: updated 10-OCT-2022 (CHAA009) no expiry
Coq Formalisation of Recursive Adaptive Grammars (available)
The aim of this project is to formalise within the Coq proof assistant [1] the meta-theory of the recursive adaptive grammar framework [2] Programming languages are usually specified on two levels. The first level defines a context-free grammar that specifies the syntax of the language. Usually, however, not all syntactically correct programs make sense, and … full description “Coq Formalisation of Recursive Adaptive Grammars (available)”
Cyclist: Verifying Programs using Cyclic Proof (available)
Cyclic proofs are a technique for proving properties inductively, or proving properties about inductively defined objects or processes. They can be used to prove logical statements, or to verify recursive programs. The Cyclist tool [1] has been developed as an automatic verification tool based on cyclic proofs. It can prove termination and verify temporal properties … full description “Cyclist: Verifying Programs using Cyclic Proof (available)”
Engineering ROTOR: a Refactoring Tool for OCaml (ongoing)
OCaml [1] is a mature functional programming language with an expressive type system. Recently, we have developed a prototype tool, called ROTOR, for automatically refactoring OCaml codebases [2]. Currently, ROTOR handles renaming of functions. This is surprisingly hard due to OCaml’s powerful module system: renaming a function in one module may actually require renaming functions … full description “Engineering ROTOR: a Refactoring Tool for OCaml (ongoing)”
Machine Learning Library for OCaml (completed)
Frameworks for machine learning include Python’s TensorFlow [1]. These frameworks provide standard ways of specifying models that can be optimised by machine learning algorithms. OCaml [2] is a mature functional programming language with an expressive type system. DecML [3] is a prototype OCaml extension that facilitates implementing machine learning tasks, based on specifying models as … full description “Machine Learning Library for OCaml (completed)”
Visitors for Generalized Algebraic Data Types in OCaml (completed)
Algebraic datatypes (ADTs) [1] are the basic method for defining how to build complex data values in functional programming languages: they specify both the basic, or atomic, values, as well as the constructors for building larger values out of smaller ones. For example, the following ADT defines generic lists that contain values of type ‘a … full description “Visitors for Generalized Algebraic Data Types in OCaml (completed)”