Add tutorials on Curry-Howard Isomorphism

[melvic-ybanez]

The following should also contain some common isomorphisms and code samples from supported languages. The user should be able to select which language to choose for the samples.

[mlliarm]

Hello,

Not exactly a tutorial, but this talk of prof. P. Wadler is an amazing introduction to the Curry-Howard Isomorphism.

If you want I can write a summary of the ideas mentioned there.

Regarding the common isomorphisms and code samples I'll have to do further research.

Overall really interesting enhancement, I'd love to work on this.

Cheers !

ps: Also these two talks of prof. Wadler [1][2] are very interesting as well, if you haven't watched them before. And finally, this paper [3] of prof. Baez is a must read, if only to keep the final result, the table with all the isomorphisms between the scientific fields mentioned there, that I believe is related to the Curry-Howard isomorphism.

---

[1] YouTube: "Everything Old is New Again: Quoted Domain Specific Languages"

[2] YouTube: "Categories for the Working Hacker"

[3] Arxiv.org: Physics, Topology, Logic and Computation: A Rosetta Stone

[melvic-ybanez]

Not exactly a tutorial, but this talk of prof. P. Wadler is an amazing introduction to the Curry-Howard Isomorphism.

Yes, I've watched this one before. It may actually be one of the resources I used to learn Curry-Howard Isomorphism. It's really useful.

@mlliarm I'd really appreciate it if you would work on this. It's good to see other people also interested in these topics.

Thanks for the links. I think I've only watched the second one.

[mlliarm]

I'd love to, @melvic-ybanez ! Thank you for creating such an interesting project !

Feel free to assign this issue to me.

If I write the tutorial/notes of the talk (and perhaps the basic ideas from Howards' paper) in Markdown, would it be okay?

Cheers !

[melvic-ybanez]

The plan is to eventually add the tutorial to the UI. So users can select a Tutorial menu item and see a new panel of explanations and examples. However, we can also have a separate task for that.

For now, it's okay to write it in Markdown, unless you also want to write the UI. I'm also open to other suggestions.

[mlliarm]

@melvic-ybanez I'll start with the Markdown and when time comes I can help with the UI, but will need some help to get started (like directions etc), because I don't know much about UI development. Thanks again.

[mlliarm]

Sorry, I got distracted from work and stuff. I'll start this week, but could take a while to have something complete.

• As step 1: extract related notes from the talk of prof. Wadler on the CH-isomorphism.
• As step 2: check Howard's paper and do a summary of the main ideas and arguments.
• As step 3: create more examples in code in some static typed functional languages (I'll start with the ones you've already used).

Edit: Actually, that speech is based on this paper (PDF) of prof. Wadler. I'll start from here.

[melvic-ybanez]

No worries @mlliarm! The steps look good to me. Thanks for taking this one.