winterkoninkje: Shadowcrane (Default)
[personal profile] winterkoninkje
This is a followup to a recent post on Parameterized Monads which I discovered independently, along with everyone else :)

For anyone interested in reading more about them, Oleg Kiselyov also discovered them independently, and developed some Haskell supporting code. Coq supporting code by Matthieu Sozeau is also available. And apparently Robert Atkey investigated them thoroughly in 2006.

If people are interested in more Coq support, I've been working on a Coq library for basic monadic coding in a desperate attempt to make programming (rather than theorem proving) viable in Coq. Eventually I'll post a link to the library which will include parameterized monads as well as traditional monads, applicative functors, and other basic category theoretic goodies. This library along with the Vecs library I never announced stemmed from work last term on proving compiler correctness for a dependently typed language. Hopefully there'll be more news about that this fall.

Date: 2010-06-13 06:20 pm (UTC)
ext_17921: (Default)
From: [identity profile] lindseykuper.livejournal.com
If people are interested in more Coq support, I've been working on a Coq library for basic monadic coding in a desperate attempt to make programming (rather than theorem proving) viable in Coq.

Have you already looked at Ynot and found it didn't do what you want?

Profile

winterkoninkje: Shadowcrane (Default)
wren gayle romano

July 2014

S M T W T F S
   12345
678 910 11 12
1314151617 1819
20212223242526
2728293031  

Most Popular Tags

Expand Cut Tags

No cut tags

Style Credit

Page generated Jul. 25th, 2014 01:32 am
Powered by Dreamwidth Studios