CommunityNews

CommunityNews

Program = Proof (PDF)

These are the extended notes for the INF551 course which I taught at École Polytechnique starting from 2019. The goal is to give a first introduction to the Curry-Howard correspondence between programs and proofs, from a theoretical programmer’s perspective: we want to understand the theory behind logic and programming languages, but also to write concrete programs (in OCaml) and proofs (in Agda). Although most of the material is self-contained, the reader is supposed to be already acquainted with logic and programming.

This thread was posted by one of our members via one of our news source trackers.

Where Next?

Popular Backend topics Top

PragmaticBookshelf
Learning Clojure involves much more than just learning the mechanics. To really get Clojure you need to understand the ideas underlying i...
New
PragmaticBookshelf
RSpec has been downloaded more than 80 million times and has inspired countless test frameworks in other languages. Myron Marston @...
New
PragmaticBookshelf
Build highly interactive applications without ever leaving Elixir, the way the experts do. Let LiveView take care of performance, scalabi...
New
PragmaticBookshelf
Develop your intuition for practical Python patterns as you use new modules and tools to write clean, efficient, and correct Python code....
New
PragmaticBookshelf
Write Python code that’s faster, safer, more idiomatic, and easier to maintain with one hundred highly-curated and sharply-focused profes...
New
PragmaticBookshelf
This project based book gets you up to speed on building and deploying Elixir IoT applications using Nerves, as you develop a real-world ...
New
PragmaticBookshelf
Level up your Rust programming skills with a series of brain teasers as you discover some of the unexpected Rust behaviors and challenge ...
New
PragmaticBookshelf
Build efficient applications that exploit the unique benefits of a pure functional language, learning from an engineer who uses Haskell t...
New
ManningBooks
Effectively reading and understanding existing code is a developer’s superpower. In this book, you’ll master techniques for code profilin...
New
PragmaticBookshelf
Get up to speed with the changes in the Java language from version 9 to 19 and apply the amazing features in your application to improve ...
New

Other popular topics Top

AstonJ
A thread that every forum needs! Simply post a link to a track on YouTube (or SoundCloud or Vimeo amongst others!) on a separate line an...
New
PragmaticBookshelf
Design and develop sophisticated 2D games that are as much fun to make as they are to play. From particle effects and pathfinding to soci...
New
New
PragmaticBookshelf
Rust is an exciting new programming language combining the power of C with memory safety, fearless concurrency, and productivity boosters...
New
New
Margaret
Hello everyone! This thread is to tell you about what authors from The Pragmatic Bookshelf are writing on Medium.
1143 25883 760
New
rustkas
Intensively researching Erlang books and additional resources on it, I have found that the topic of using Regular Expressions is either c...
New
AstonJ
Saw this on TikTok of all places! :lol: Anyone heard of them before? Lite:
New
foxtrottwist
A few weeks ago I started using Warp a terminal written in rust. Though in it’s current state of development there are a few caveats (tab...
New
PragmaticBookshelf
Programming Ruby is the most complete book on Ruby, covering both the language itself and the standard library as well as commonly used t...
New