Type theory and functional programming

Mentions per year

What Hacker News says

• codeismath · Aug 7, 2025 · Recommends

  Books. Some books on my shelf covering these topics: "Type Theory and Functional Programming" by Simon Thompson (PDF available via quick search) First 120 pages of "Type Theory and Formal Proof" by Rob Nederpelt / Herman Geuvers For some early stuff on dependent types (also covered in the above),…

  on “Why is it worth spending time on type theory? (2013)” ↗
• solomatov · Apr 21, 2014 · Recommends

  …calculus of inductive constructions, which is a similar formalism to MLTT) first, and learn to write code later. Otherwise everything will seem like a magic. There are however, good books on the topic: * Type Theory and Functional Programming (http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/) * Programming in Martin-Lof type theory (http://www.cse.chalmers.se/research/group/logic/book/)

  on “The Case for Formal Verification (2013)” ↗
• siraben · May 24, 2021 · Mentions

  …might prove some type-theoretic thing like type preservation). There's also a range of type theory books because it's a field that spans pure logic to programming languages, so you can find books like Type Theory and Functional Programming by Thompson that elaborate things like dependent types early on.

  on “Counterexamples in Type Systems” ↗
• codeismath · May 24, 2021 · Mentions

  …until picking up Type Theory and Formal Proof. This one took me somewhere between 100 to 200 pages before getting lost. They cover the entire lambda cube. But then I was able to re-start Thompson's "Type Theory and Functional Programming" and it was clear that I started to understand a lot of it. If you enjoy the nostalgia of older books like me, then pick up an original copy of "Intuitionistic Type Theory" edited by Per Martin-Löf.

  on “Counterexamples in Type Systems” ↗
• silentvoice · Mar 31, 2014 · Mentions

  …univalent foundations it sounds like they are adding magic sauce to make this possible, and so I follow it closely (but don't understand it all yet). The interesting path I spoke of earlier: I'm now learning type theory and functional programming just so that I can make sense of this branch of computer science that I originally didn't know existed.

  on “Univalent Foundations: New Foundations of Mathematics [video]” ↗
• chriswarbo · May 27, 2014 · Mentions

  Indeed, the wording of the article even made me think of type theory and functional programming. > For instance, a kettle with a power supply can serve as a constructor that can perform the task of heating water. kettle power_supply water : (water * heat) > You simply say that the task of creating…

  on “A New “Theory of Everything”: Reality Emerges from Cosmic Copyright Law” ↗