search

langston-barrett / CoverTranslator

A tool for formally verifying Haskell code in Agda
MIT License
28 stars 0 forks source link

Support Agda 2 #2

Open langston-barrett opened 8 years ago

ichistmeinname commented 8 years ago

Is there already a key idea regarding the monadic translation? I tried to use the approach of the mentioned paper to formalise a construction in Coq, but it wouldn't work as hoped because of non-strictly positive occurrences of type variables in the monadic translation. Is this a problem in Agda2 as well and does it need to be tackled? If so, what's your idea for the translation?

langston-barrett commented 8 years ago

@ichistmeinname I don't really have an idea for the translation, this is mostly brainstorming for now :smile: Sorry!

ichistmeinname commented 8 years ago

Ah, I see. If you do tackle that someday, I'd be very interested to hear more about it ; )