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
Ruby on Rails helps you produce high-quality, beautiful-looking web applications quickly—you concentrate on creating the application, and...
New
PragmaticBookshelf
Using Erlang, you’ll be surprised at how easy it becomes to deal with parallel problems, and how much faster and more efficiently your pr...
New
PragmaticBookshelf
TDD is a modern programming practice that all C developers need to know. It’s a different way to program—unit tests are written in a tigh...
New
PragmaticBookshelf
Expand your knowledge of the Raspberry Pi while building nearly a dozen immediately applicable hardware and software projects. Use Python...
New
PragmaticBookshelf
Use WebRTC to build web applications that stream media and data in real time directly from one user to another, all in the browser. ...
New
PragmaticBookshelf
Build a working binary clock using Elixir, Nerves, and OTP. Control complexity in your projects using a layered approach to software desi...
New
PragmaticBookshelf
Put the data that runs your business to work for you. Embed data governance into your practice, and build processes to data during and af...
New
ManningBooks
Fully updated to Elixir 1.14, this authoritative bestseller reveals how Elixir tackles problems of scalability, fault tolerance, and high...
New
PragmaticBookshelf
Leverage serverless technologies on Cloudflare's global platform to build a variety of applications more easily and quickly. Ashley ...
New
PragmaticBookshelf
A concise guide to MySQL 9 database administration, covering fundamental concepts, techniques, and best practices. Neil Smyth MySQL...
New

Other popular topics Top

Exadra37
I am thinking in building or buy a desktop computer for programing, both professionally and on my free time, and my choice of OS is Linux...
New
New
AstonJ
There’s a whole world of custom keycaps out there that I didn’t know existed! Check out all of our Keycaps threads here: https://forum....
New
AstonJ
Just done a fresh install of macOS Big Sur and on installing Erlang I am getting: asdf install erlang 23.1.2 Configure failed. checking ...
New
AstonJ
Do the test and post your score :nerd_face: :keyboard: If possible, please add info such as the keyboard you’re using, the layout (Qw...
New
AstonJ
In case anyone else is wondering why Ruby 3 doesn’t show when you do asdf list-all ruby :man_facepalming: do this first: asdf plugin-upd...
New
PragmaticBookshelf
Learn different ways of writing concurrent code in Elixir and increase your application's performance, without sacrificing scalability or...
New
PragmaticBookshelf
Build highly interactive applications without ever leaving Elixir, the way the experts do. Let LiveView take care of performance, scalabi...
New
New
PragmaticBookshelf
Develop, deploy, and debug BEAM applications using BEAMOps: a new paradigm that focuses on scalability, fault tolerance, and owning each ...
New