FreeProving/free-compiler
A Haskell to Coq compiler that represents effectful programs with the free monad
HaskellBSD-3-Clause
Issues
- 0
Agda-2.6.* dependency leads to errors
#225 opened by javiergarea - 0
- 0
Adapt Coq examples to the new usability changes
#164 opened by MarvinLira - 0
Update Pattern Matching Compiler
#210 opened by just95 - 0
Instance arguments in sections
#204 opened by just95 - 0
- 0
- 0
- 0
Generate enhanced induction schemes
#159 opened by MarvinLira - 0
- 3
Detect effects in functions
#134 opened by MajaRet - 0
Generate Normalform instances
#150 opened by MajaRet - 1
Generate ShareableArgs instances
#151 opened by MajaRet - 0
- 0
Global variables are not shared
#214 opened by MajaRet - 0
- 0
Implement an analysis of the order of let bindings
#158 opened by maclement - 0
Add `call` operator to the lifted IR
#196 opened by Daniel-Teut - 0
Handlers induce strictness in proofs
#208 opened by MajaRet - 0
Inconsistent sharing behavior for effects in Haskell
#181 opened by MajaRet - 0
Synchronize `main` and `dev-case-studies` branch
#185 opened by MarvinLira - 0
Allow aliases in decreasing arguments analysis
#192 opened by just95 - 0
Wrong type is inferred for `let` expressions
#190 opened by just95 - 0
- 0
Implement Handler typeclass
#177 opened by MajaRet - 1
- 0
- 0
Add a `share` operator to the lifted IR
#176 opened by Daniel-Teut - 0
- 0
Implement ShareableArgs typeclass
#149 opened by MajaRet - 0
Add compiler flag for evaluation strategy
#168 opened by Daniel-Teut - 0
Generate simplification lemmas
#182 opened by MarvinLira - 0
Implement Normalform typeclass
#148 opened by MajaRet - 1
Check whether notation-scopes should be used
#178 opened by MarvinLira - 0
Differing type parameters in mutually recursive types produce invalid Coq code
#172 opened by MajaRet - 0
Switch from `Ltac` to `Ltac2`
#165 opened by MarvinLira - 0
- 0
Generate induction schemes
#154 opened by MarvinLira - 0
Implement polymorphic let bindings
#157 opened by maclement - 0
Generate agda-lib file
#142 opened by JonasHoefer - 0
Implement type classes for sharing and tracing
#137 opened by MajaRet - 0
Translate quick check properties to Agda
#146 opened by JonasHoefer - 0
Generate mutual recursive agda data types
#145 opened by JonasHoefer - 0
Generate mutual recursive agda functions
#144 opened by JonasHoefer - 0
Expand Agda base library
#121 opened by JonasHoefer - 0
Built-in operators evaluate arguments in wrong order
#133 opened by just95 - 0
Construct an effect-generic sharing handler
#125 opened by MajaRet - 0
Agda case studies
#124 opened by JonasHoefer - 0
Implement a tracing effect in Coq
#120 opened by MajaRet - 0