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
Real-time applications come with real challenges—persistent connections, multi-server deployment, and strict performance requirements are...
New
PragmaticBookshelf
Is your current programming language ready for tomorrow? Elixir is. Elixir is a modern, functional language built on the Erlang VM. ...
New
PragmaticBookshelf
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
PragmaticBookshelf
Construct, analyze, and visualize networks with networkx, a Python language module. Discover how to work with social, product, temporal, ...
New
PragmaticBookshelf
You want increased customer satisfaction, faster development cycles, and less wasted work. Domain-driven design (DDD) and functional prog...
New
PragmaticBookshelf
Go from messy, unstructured artifacts stored in SQL and NoSQL databases to a neat, well-organized dataset with this quick reference for t...
New
PragmaticBookshelf
Communicate more clearly, refactor more effectively, and save time with attractive diagrams that only take minutes to make with open sour...
New
ManningBooks
Spring Security in Action, Second Edition is a revised version of the bestselling original, fully updated for Spring Boot 3 and Oauth2/Op...
New
PragmaticBookshelf
Give your Rail's apps an instant performance boost by harnessing the power of efficient, manageable, and sustainable background processin...
New
PragmaticBookshelf
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 Top

AstonJ
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
AstonJ
Curious to know which languages and frameworks you’re all thinking about learning next :upside_down_face: Perhaps if there’s enough peop...
New
AstonJ
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
AstonJ
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
PragmaticBookshelf
Author Spotlight James Stanier @jstanier James Stanier, author of Effective Remote Work , discusses how to rethink the office as we e...
New
husaindevelop
Inside our android webview app, we are trying to paste the copied content from another app eg (notes) using navigator.clipboard.readtext ...
New
PragmaticBookshelf
Author Spotlight: Sophie DeBenedetto @SophieDeBenedetto The days of the traditional request-response web application are long gone, b...
New
First poster: bot
zig/http.zig at 7cf2cbb33ef34c1d211135f56d30fe23b6cacd42 · ziglang/zig. General-purpose programming language and toolchain for maintaini...
New
New
CommunityNews
A Brief Review of the Minisforum V3 AMD Tablet. Update: I have created an awesome-minisforum-v3 GitHub repository to list information fo...
New