[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Logic as an implementation language
> I can find lots of work on compiler verification, but nothing where
> the logic of a theorem prover has been used as a functional
> programming language. Does anyone on this list have any good pointers
> or hints where to look?
I did some work on FP-in-HOL for my PhD:
The main emphasis was to see how much of the core of contemporary
functional programming languages like ML can be modelled directly by the
functions of higher order logic. It's no surprise that this can be done
in principle; the work was in providing the pattern-matching facilities
that FP'ers expect, and in supporting various styles of recursion
(mutual and nested in particular).