Re: Formal semantics of language semantics

"Joachim Durchholz" <joachim_d@gmx.de> writes:
> As a loosely related example, consider the ML family of languages.
> Initially, there was a theorem prover, the language for specifying
> theorems and proofs being ML. (I don't know whether that prover was
> ever used to specify programming language semantics. It would have
> been possible, because if you have a constructive proof that a
> function exists, that proof can be automatically transformed into a
> program that computes the function.)

That system was LCF, and a close descendent of LCF is HOL. HOL has
indeed been used to describe program language semantics: try googling
for "HOL semantics programming". Most of the examples are for toy
languages, but some seem to be for real languages.

-Lex

Return to the comp.compilers page.
Search the comp.compilers archives again.