Re: Formal semantics of language semantics

"Lex Spoon" <lex@cc.gatech.edu>
13 Oct 2002 16:00:45 -0400

          From comp.compilers

Related articles
[5 earlier articles]
Re: Formal semantics of language semantics stephen@dino.dnsalias.com (Stephen J. Bevan) (2002-09-29)
Re: Formal semantics of language semantics lex@cc.gatech.edu (Lex Spoon) (2002-09-29)
Re: Formal semantics of language semantics whopkins@alpha2.csd.uwm.edu (Mark) (2002-09-29)
Re: Formal semantics of language semantics nmm1@cus.cam.ac.uk (Nick Maclaren) (2002-10-13)
Re: Formal semantics of language semantics haberg@matematik.su.se (Hans Aberg) (2002-10-13)
Re: Formal semantics of language semantics scgupta@solomons.cs.uwm.edu (Satish C. Gupta) (2002-10-13)
Re: Formal semantics of language semantics lex@cc.gatech.edu (Lex Spoon) (2002-10-13)
Re: Formal semantics of language semantics anw@merlot.uucp (Dr A. N. Walker) (2002-10-18)
Re: Formal semantics of language semantics whopkins@alpha2.csd.uwm.edu (Mark) (2002-10-18)
Re: Formal semantics of language semantics whopkins@alpha2.csd.uwm.edu (Mark) (2002-10-18)
Re: Formal semantics of language semantics nmm1@cus.cam.ac.uk (Nick Maclaren) (2002-10-20)
Re: Formal semantics of language semantics nmm1@cus.cam.ac.uk (Nick Maclaren) (2002-10-20)
Re: Formal semantics of language semantics merlot!anw@mailbox1.ucsd.edu (Dr A. N. Walker) (2002-10-25)
[5 later articles]
| List of all articles for this month |

From: "Lex Spoon" <lex@cc.gatech.edu>
Newsgroups: comp.compilers
Date: 13 Oct 2002 16:00:45 -0400
Organization: Georgia Institute of Technology
References: 02-09-149 02-09-163
Keywords: semantics
Posted-Date: 13 Oct 2002 16:00:44 EDT

"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


Post a followup to this message

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