Programming Languages, Martials Arts and Computers. The Weblog of Chris Double.
SWI Prolog is an open source Prolog implementation with good documentation and many interesting libraries. One library that was published recently is Web Prolog. While branded as a 'Web Logic Programming Language' the implementation in the github repository runs under SWI Prolog and adds Erlang style distributed concurrency. There is a PDF Book in the repository that goes into detail... more →
I've been reading the book Building High Integrity Applications with Spark to learn more about the [SPARK/Ada](https://en.wikipedia.org/wiki/SPARK_(programming_language)) language for formal verification. It's a great book that goes through lots of examples of how to do proofs in Spark. I wrote a post on Spark/Ada earlier this year and tried some of the examples in the GNAT edition. While working through... more →
This post covers using the latest version of ATS, ATS 2, and goes through proving some basic algorithms. I've written a couple of posts before on using proofs in ATS 1: more →
The ATS programming language has a powerful type and proof system to enable safe construction of programs. Sometimes there is a need to cast a value from one type to another. ATS provides a feature that enables the programming to write their own rules specifying what can be cast. This becomes important when converting types from non-dependent typed values to... more →
A few years ago I wrote a mailing list post on cross compiling ATS to Android. With ATS2 being released the ability to cross compile has been made easier. In this post I'll show how to produce static linux binaries using musl libc and how to build Android and Windows ATS programs by cross compiling on linux. For these examples... more →