Re: Integrated theorem prover in compiler

bart demoen <bmd@cs.kuleuven.be>
Wed, 19 Aug 2009 16:13:24 +0000 (UTC)

          From comp.compilers
Related articles
Integrated theorem prover in compiler cdegouw@gmail.com (- -) (2009-08-19)
Re: Integrated theorem prover in compiler bmd@cs.kuleuven.be (bart demoen) (2009-08-19)
Re: Integrated theorem prover in compiler walter@bytecraft.com (Walter Banks) (2009-08-19)
Re: Integrated theorem prover in compiler pertti.kellomaki@tut.fi (Pertti Kellomaki) (2009-08-20)
Re: Integrated theorem prover in compiler torbenm@pc-003.diku.dk (2009-08-20)
Re: Integrated theorem prover in compiler gneuner2@comcast.net (George Neuner) (2009-08-20)
Re: Integrated theorem prover in compiler bobduff@shell01.TheWorld.com (Robert A Duff) (2009-08-20)
Integrated theorem prover in compiler MSITARA@clemson.edu (Murali Sitaraman) (2009-10-16)
| List of all articles for this month |
From: bart demoen <bmd@cs.kuleuven.be>
Newsgroups: comp.compilers
Date: Wed, 19 Aug 2009 16:13:24 +0000 (UTC)
Organization: BELNET - The Belgian Research Network
References: 09-08-030
Keywords: theory, optimize
Posted-Date: 20 Aug 2009 10:24:55 EDT

On Wed, 19 Aug 2009 01:57:57 -0700, - - wrote:




> My question is: is there any compiler (for Eiffel, Java or any other
> language) that statically checks assertions, and if so, does it exploit
> any of the three advantages listed above?


Have a look at CIAO Prolog http://clip.dia.fi.upm.es/Software/Ciao/
It has assertions that are checked at compile time - maybe not what you
are after, but worth checking out.
AFAIK, the assertion language is extensible and so are the checkers.
Get in touch with Manuel Hermenegildo and/or Manuel Carro.


Cheers


Bart Demoen


Post a followup to this message

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