Trusted source translation of a total function language
TACAS, pp. 471-485, 2008.
total function languagesimple intermediate codehol theorem provertrusted source translationspecification languageMore(13+)
We present a trusted source translator that transforms total functions defined in the specification language of the HOL theorem prover to simple intermediate code. This translator eliminates polymorphism by code specification, removes higher-order functions through closure conversion, interprets pattern matching as conditional expressions...More
Full Text (Upload PDF)
PPT (Upload PPT)