[PRL] Fwd: visit

Karl Lieberherr lieber at ccs.neu.edu
Fri Oct 6 11:07:06 EDT 2006


Hi Matthias:

I have reactivated my work on automatic theorem proving from 30 years ago and
found it to be used in all state-of-the-art SAT solvers. The paper on
Superreolution is currently on SAT Live

http://www.satlive.org/

with the highest number of hits among the last 10 postings. This work
is actually useful
in biology because SAT solvers solve very successfully huge instances
of combinatorial optimization problems appearing in biology.

Looking forward to talk to Cormac.

-- Karl

On 10/6/06, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
> Cormac Flanagan on October 19 -- Matthias
>
>
> Begin forwarded message:
>
> > Title:    Hybrid Type Checking for Flexible Specifications
> >
> > Abstract:
> >
> > Software systems typically contain large APIs that are informally
> > specified and hence easily misused. This talk
> > describes the Sage programming language, which is designed
> > to support and enforce precise yet flexible interface specifications.
> > In additional to traditional static types, the Sage type system
> > also supports first-class types and arbitrary refinement types.
> > Sage enforces these specifications using a combination of
> > static type checking, dynamic contract checking, automatic theorem
> > proving,
> > and a database of historical specification violations.
>
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl
>



More information about the PRL mailing list