[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