
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

Learning Clojure involves much more than just learning the mechanics. To really get Clojure you need to understand the ideas underlying i...
New

RSpec has been downloaded more than 80 million times and has inspired countless test frameworks in other languages.
Myron Marston @...
New

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

Develop your intuition for practical Python patterns as you use new modules and tools to write clean, efficient, and correct Python code....
New

Write Python code that’s faster, safer, more idiomatic, and easier to maintain with one hundred highly-curated and sharply-focused profes...
New

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

Level up your Rust programming skills with a series of brain teasers as you discover some of the unexpected Rust behaviors and challenge ...
New

Build efficient applications that exploit the unique benefits of a pure functional language, learning from an engineer who uses Haskell t...
New

Effectively reading and understanding existing code is a developer’s superpower. In this book, you’ll master techniques for code profilin...
New

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

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

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

Rust is an exciting new programming language combining the power of C with memory safety, fearless concurrency, and productivity boosters...
New

Think Again 50% Off Sale »
The theme of this sale is new perspectives on familiar topics.
Enter coupon code ThinkAgain2021 at checkout t...
New

Hello everyone! This thread is to tell you about what authors from The Pragmatic Bookshelf are writing on Medium.
New

Intensively researching Erlang books and additional resources on it, I have found that the topic of using Regular Expressions is either c...
New

Saw this on TikTok of all places! :lol:
Anyone heard of them before?
Lite:
New

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

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
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
- /crystal
- /kotlin
- /c-plus-plus
- /tailwind
- /gleam
- /react
- /ocaml
- /elm
- /flutter
- /vscode
- /ash
- /html
- /opensuse
- /centos
- /php
- /deepseek
- /zig
- /scala
- /lisp
- /sublime-text
- /textmate
- /nixos
- /debian
- /react-native
- /agda
- /kubuntu
- /arch-linux
- /django
- /revery
- /ubuntu
- /spring
- /manjaro
- /nodejs
- /diversity
- /lua
- /julia
- /c
- /slackware
- /markdown