3 ms·

Do you have any project ideas for Agda? I used it to formalize the simply typed lambda calculus; what else should I do? After all, I can't really do "traditiona

Do you have any project ideas for Agda? I used it to formalize the simply typed lambda calculus; what else should I do? After all, I can't really do "traditional" programming projects in Agda as its ecosystem is more geared towards proving. Are there any interesting projects with proofs as a focus?

m_j_g 6y ago
I currently need help with: - (you can make it your own project) type-safe library for Matroids (in cubical agda, so different representations can be handled automatically) - If you have some Elm experience you can help me with online toy to play with cubical agda :) ( https://raw.githack.com/marcinjangrzybowski/cubeViz/master/main.html#assoc,assoc https://raw.githack.com/marcinjangrzybowski/cubeViz/master/m... In fact I would be very happy to find a collaborator for those projects. There is lot of people from academia focused on the fundamental projects, but I am more focused in programming something practical.
- TheAsprngHacker 6y ago
  Wow, cool! I'm still wrapping my head around Cubical Type Theory, so I'm not sure if I can help. I don't have the mathematical background to know what Matroids are (skimming the Wikipedia page, I see some set-theory-centric definitions that talk about subsets and powersets, to what extent would they translate to type theory?).
  - m_j_g 6y ago
    There is nothing special about them. I am talking about simple formalisation, there is already some code about finite types in cubical-agda library, so it would be good place to start. I think that usefull definitions and properties can be formalised in ~100h. Matroids are known to be good example of cryptomorphic structures, so cubical agda can be used so that those cryptohmorphism can work "under the hood". I know how to do this, but I am currently working on something different. If You are interested pm me.

m_j_g 6y ago

I currently need help with: - (you can make it your own project) type-safe library for Matroids (in cubical agda, so different representations can be handled automatically) - If you have some Elm experience you can help me with online toy to play with cubical agda :) ( https://raw.githack.com/marcinjangrzybowski/cubeViz/master/main.html#assoc,assoc https://raw.githack.com/marcinjangrzybowski/cubeViz/master/m... In fact I would be very happy to find a collaborator for those projects. There is lot of people from academia focused on the fundamental projects, but I am more focused in programming something practical.

TheAsprngHacker 6y ago
Wow, cool! I'm still wrapping my head around Cubical Type Theory, so I'm not sure if I can help. I don't have the mathematical background to know what Matroids are (skimming the Wikipedia page, I see some set-theory-centric definitions that talk about subsets and powersets, to what extent would they translate to type theory?).
- m_j_g 6y ago
  There is nothing special about them. I am talking about simple formalisation, there is already some code about finite types in cubical-agda library, so it would be good place to start. I think that usefull definitions and properties can be formalised in ~100h. Matroids are known to be good example of cryptomorphic structures, so cubical agda can be used so that those cryptohmorphism can work "under the hood". I know how to do this, but I am currently working on something different. If You are interested pm me.