
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.
Popular Backend topics

Ruby on Rails helps you produce high-quality, beautiful-looking web applications quickly—you concentrate on creating the application, and...
New

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

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

Expand your knowledge of the Raspberry Pi while building nearly a dozen immediately applicable hardware and software projects. Use Python...
New

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

Build a working binary clock using Elixir, Nerves, and OTP. Control complexity in your projects using a layered approach to software desi...
New

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

Fully updated to Elixir 1.14, this authoritative bestseller reveals how Elixir tackles problems of scalability, fault tolerance, and high...
New

Leverage serverless technologies on Cloudflare's global platform to build a variety of applications more easily and quickly.
Ashley ...
New

A concise guide to MySQL 9 database administration, covering fundamental concepts, techniques, and best practices.
Neil Smyth
MySQL...
New
Other popular topics

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

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

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

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

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

Learn different ways of writing concurrent code in Elixir and increase your application's performance, without sacrificing scalability or...
New

Build highly interactive applications without ever leaving Elixir, the way the experts do. Let LiveView take care of performance, scalabi...
New

Author Spotlight
Dmitry Zinoviev
@aqsaqal
Today we’re putting our spotlight on Dmitry Zinoviev, author of Data Science Essentials in ...
New

Develop, deploy, and debug BEAM applications using BEAMOps: a new paradigm that focuses on scalability, fault tolerance, and owning each ...
New
Categories:
Sub Categories:
Popular Portals
- /elixir
- /rust
- /wasm
- /ruby
- /erlang
- /phoenix
- /keyboards
- /rails
- /js
- /python
- /security
- /go
- /swift
- /vim
- /clojure
- /emacs
- /haskell
- /java
- /onivim
- /typescript
- /svelte
- /kotlin
- /crystal
- /c-plus-plus
- /tailwind
- /react
- /gleam
- /ocaml
- /elm
- /flutter
- /vscode
- /ash
- /html
- /opensuse
- /centos
- /php
- /deepseek
- /zig
- /scala
- /textmate
- /sublime-text
- /lisp
- /debian
- /nixos
- /react-native
- /agda
- /kubuntu
- /arch-linux
- /django
- /ubuntu
- /revery
- /spring
- /manjaro
- /nodejs
- /diversity
- /deno
- /lua
- /julia
- /slackware
- /c