OCaml to LambdaProlog

• 

  The OCaml file and the output from translating it to LambdaProlog.

• 

  The signature and module files resulting from the translation of the file in the first picture.

What it does

This project takes a restricted subset* of the syntax of OCaml and builds a LambdaProlog specification for the code. This can be used to reason about the software and prove that it has certain properties using the Abella theorem prover. This allows us to be certain that our software has the properties we desire.

How I built it

I parsed the OCaml file to get the new type definitions and functions out in Python, since I don't know how to use OCaml's parsing abilities, and then transformed these to LambdaProlog definitions.

Challenges I ran into

Setting up parsing by hand is extremely challenging. My main difficulties were in parsing and then using the result of my parsing method to identify recursive function calls.

What's next for OCaml to LambdaProlog

The Python incarnation of OCaml to LambdaProlog is probably done, but the idea behind it will live on. I believe using OCaml's parsing abilities to parse the file will lead to more robust parsing and allow a larger subset of OCaml's syntax to be used, and intend to look into this in the future.

Prompt

No, this does not have anything to do with the prompt. However, I think it is interesting anyway.

• A few of the restrictions I placed to simplify parsing: all functions must be annotated with their types, identifier assignments are not permitted other than for functions, there may not be an "else" without a following "if", and functions may not make more than one recursive call in any instance.

Built With

• python