Re: Integrated theorem prover in compiler

Pertti Kellomaki <pertti.kellomaki@tut.fi>
Thu, 20 Aug 2009 09:55:35 +0300

          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: Pertti Kellomaki <pertti.kellomaki@tut.fi>
Newsgroups: comp.compilers
Date: Thu, 20 Aug 2009 09:55:35 +0300
Organization: Compilers Central
References: 09-08-030
Keywords: theory, optimize
Posted-Date: 20 Aug 2009 10:26:05 EDT

- - 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?


There is at least SPARK Ada <http://www.praxis-his.com/sparkada/>,
and the toolsets associated with the B-method
<http://en.wikipedia.org/wiki/B-Method>.


You might also want to take a look at PVS <http://pvs.csl.sri.com/>
which kind of does it the other way around. There is a subset
of the theorem prover language that can be used as a functional
programming language, and mapped to Common Lisp. Not exactly
what you are asking for, but quite related. I just love the
predicate subtype mechanism in the language.


There is also Coq and other theorem provers where it is possible
to derive programs from proofs, but that is (at least to me)
quite a bit hairier.
--
Pertti


Post a followup to this message

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