[Haskell-cafe] funct.prog. vs logic prog., practical Haskell
Petr Pudlak
deb at pudlak.name
Sun Aug 2 09:26:19 EDT 2009
That's actually a good idea. I haven't considered this alternative so far,
probably because I have always been working with first-order theorem provers.
But I guess eventually I'll merge my interests in ATP and FP and start doing
some serious work with higher-order theorem provers like coq or Isabelle.
Petr
On Sun, Aug 02, 2009 at 09:03:14AM -0400, Carter Schonwald wrote:
> Have you considered say proposing a class on theorem proving that uses coq?
> www.coq.inria.fr . Such a class would entail teaching how to program using the
> coq term language, which is itself a pure functional language, albeit one with
> some restrictions related to everything impure. As a matter of course in such
> a class you would naturally also mention that there are languages such as
> haskell which lack such restrictions/ have clever ways around them.
>
> -Carter
>
> On Sun, Aug 2, 2009 at 8:52 AM, Petr Pudlak <deb at pudlak.name> wrote:
> I'm a faculty member (postdoc). I've been working in the field of
> automated
> theorem proving, but for about a year I'm also very interested in Haskell
> and
> in general in the theory behind functional languages. Since I find FP to
> be a
> very important programming concept, I'd like to achieve that we start
> teaching
> it at the university.
>
> Petr
>
>
>
More information about the Haskell-Cafe
mailing list