
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

Real-time applications come with real challenges—persistent connections, multi-server deployment, and strict performance requirements are...
New

Is your current programming language ready for tomorrow? Elixir is. Elixir is a modern, functional language built on the Erlang VM.
...
New

Your domain is rich and interconnected, and your API should be, too. Upgrade your web API to GraphQL, using flexible queries to empower y...
New

Construct, analyze, and visualize networks with networkx, a Python language module. Discover how to work with social, product, temporal, ...
New

You want increased customer satisfaction, faster development cycles, and less wasted work. Domain-driven design (DDD) and functional prog...
New

Go from messy, unstructured artifacts stored in SQL and NoSQL databases to a neat, well-organized dataset with this quick reference for t...
New

Communicate more clearly, refactor more effectively, and save time with attractive diagrams that only take minutes to make with open sour...
New

Spring Security in Action, Second Edition is a revised version of the bestselling original, fully updated for Spring Boot 3 and Oauth2/Op...
New

Give your Rail's apps an instant performance boost by harnessing the power of efficient, manageable, and sustainable background processin...
New

Explore the power of Ash Framework by modeling and building the domain for a real-world web application.
Rebecca Le @sevenseacat and ...
New
Other popular topics

If it’s a mechanical keyboard, which switches do you have?
Would you recommend it? Why?
What will your next keyboard be?
Pics always w...
New

Curious to know which languages and frameworks you’re all thinking about learning next :upside_down_face:
Perhaps if there’s enough peop...
New

Thanks to @foxtrottwist’s and @Tomas’s posts in this thread: Poll: Which code editor do you use? I bought Onivim! :nerd_face:
https://on...
New

This looks like a stunning keycap set :orange_heart:
A LEGENDARY KEYBOARD LIVES ON
When you bought an Apple Macintosh computer in the e...
New

Author Spotlight
James Stanier
@jstanier
James Stanier, author of Effective Remote Work , discusses how to rethink the office as we e...
New

Inside our android webview app, we are trying to paste the copied content from another app eg (notes) using navigator.clipboard.readtext ...
New

Author Spotlight:
Sophie DeBenedetto
@SophieDeBenedetto
The days of the traditional request-response web application are long gone, b...
New

zig/http.zig at 7cf2cbb33ef34c1d211135f56d30fe23b6cacd42 · ziglang/zig.
General-purpose programming language and toolchain for maintaini...
New

Will Swifties’ war on AI fakes spark a deepfake porn reckoning?
New

A Brief Review of the Minisforum V3 AMD Tablet.
Update: I have created an awesome-minisforum-v3 GitHub repository to list information fo...
New
Categories:
Sub Categories:
Popular Portals
- /elixir
- /rust
- /ruby
- /wasm
- /erlang
- /phoenix
- /keyboards
- /rails
- /js
- /python
- /security
- /go
- /swift
- /vim
- /clojure
- /emacs
- /java
- /haskell
- /onivim
- /svelte
- /typescript
- /crystal
- /c-plus-plus
- /kotlin
- /tailwind
- /gleam
- /react
- /ocaml
- /flutter
- /elm
- /vscode
- /ash
- /opensuse
- /centos
- /php
- /deepseek
- /html
- /zig
- /scala
- /textmate
- /sublime-text
- /debian
- /nixos
- /lisp
- /agda
- /react-native
- /kubuntu
- /arch-linux
- /revery
- /ubuntu
- /manjaro
- /spring
- /django
- /diversity
- /lua
- /nodejs
- /slackware
- /julia
- /c
- /markdown