Backend>Learning Resources

Program = Proof (PDF)

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.

View thread on forum
/ocaml/agda#pdf
0 1607 0

Where Next?

View thread on forum
ocaml
agda
pdf
Home Backend>Learning Resources
/ocaml/agda#pdf
0 1607 0
Last post

Popular Backend topics Top

PragmaticBookshelf
Backend>Learning Resources

Real-Time Phoenix
Real-time applications come with real challenges—persistent connections, multi-server deployment, and strict performance requirements are...
pragprog.com
#pragprog/elixir/phoenix/book-real-time-phoenix#published-book
22 3337 4
New
PragmaticBookshelf
Backend>Learning Resources

Craft GraphQL APIs in Elixir with Absinthe
Your domain is rich and interconnected, and your API should be, too. Upgrade your web API to GraphQL, using flexible queries to empower y...
pragprog.com
#pragprog/elixir#published-book#api/book-craft-graphql-apis-in-elixir-with-absinthe
22 3476 10
New
PragmaticBookshelf
Backend>Learning Resources

Metaprogramming Elixir
Chris McCord edited by Jacquelyn Carter @jkcarter Metaprogramming is one of Elixir’s greatest features. Maybe you’ve played with the bas...
pragprog.com
#pragprog/elixir#published-book/book-metaprogramming-elixir
3 3119 0
New
PragmaticBookshelf
Backend>Learning Resources

Programming Erlang (2nd edition)
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...
pragprog.com
#pragprog/erlang#published-book/book-programming-erlang-2nd-edition
5 3435 0
New
PragmaticBookshelf
Backend>Learning Resources

Python Brain Teasers
Get ready for 30 teasers that will hone your Python skills and challenge your brain.. Miki Tebeka @tebeka edited by Margaret Eldridg...
pragprog.com
#pragprog/python#published-book/book-python-brain-teasers
9 3245 2
New
PragmaticBookshelf
Backend>Learning Resources

Intuitive Python
Develop your intuition for practical Python patterns as you use new modules and tools to write clean, efficient, and correct Python code....
pragprog.com
#pragprog/python#published-book/book-intuitive-python
5 4032 1
New
PragmaticBookshelf
Backend>Learning Resources

Exploring Graphs with Elixir
This hands-on book will quickly get you building, querying, and comparing graph data models using a robust, concurrent programming langua...
pragprog.com
#pragprog/elixir#published-book/book-exploring-graphs-with-elixir
34 5061 6
New
PragmaticBookshelf
Backend>Learning Resources

Pythonic Programming
Write Python code that’s faster, safer, more idiomatic, and easier to maintain with one hundred highly-curated and sharply-focused profes...
pragprog.com
#pragprog/python#published-book/book-pythonic-programming
11 4412 2
New
PragmaticBookshelf
Backend>Learning Resources

Agile Web Development with Rails 7
Rails 7 completely redefines what it means to produce fantastic user experiences and provides a way to achieve all the benefits of single...
pragprog.com
#pragprog#web-development/ruby/rails#published-book/book-agile-web-development-with-rails-7
32 6600 9
New
PragmaticBookshelf
Backend>Learning Resources

Effective Go Recipes
Shave countless hours off development time with production-ready Go recipes. Learn language nuances while doing common (and not so common...
pragprog.com
#pragprog/go#published-book/book-effective-go-recipes
4 3320 2
New

Other popular topics Top

PragmaticBookshelf
Backend>Learning Resources

Web Development with Clojure, Third Edition
Stop developing web apps with yesterday’s tools. Today, developers are increasingly adopting Clojure as a web-development platform. See f...
pragprog.com
#pragprog#web-development/clojure#published-book/book-web-development-with-clojure-third-edition
5 4584 1
New
Exadra37
General Dev>Hardware

What monitor(s) do you have for programming?
Please tell us what is your preferred monitor setup for programming(not gaming) and why you have chosen it. Does your monitor have eye p...
#monitors#coding#programming#development
227 11362 88
New
brentjanderson
General Dev>Hardware

Moonlander Keyboard (Mechanical) (Ergonomic) (Split) (Ortholinear)
Bought the Moonlander mechanical keyboard. Cherry Brown MX switches. Arms and wrists have been hurting enough that it’s time I did someth...
#hardware/keyboards#moonlander#mechanical-keyboards#ortholinear#ergonomic
212 17779 90
New
AstonJ
General Dev>Hardware

Keyboard thock (sound)
I’ve been hearing quite a lot of comments relating to the sound of a keyboard, with one of the most desirable of these called ‘thock’, he...
/keyboards#mechanical-keyboards
14 11197 8
New
AstonJ
General Dev>Code Editors

Onivim 2 Code Editor
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...
#code-editors/onivim/revery
88 6144 32
New
PragmaticBookshelf
Backend>Learning Resources

Concurrent Data Processing in Elixir
Learn different ways of writing concurrent code in Elixir and increase your application's performance, without sacrificing scalability or...
pragprog.com
#pragprog/elixir#published-book/book-concurrent-data-processing-in-elixir
78 6059 24
New
foxtrottwist
General Dev>Dev Chat

Warp—The blazingly fast, Rust-based terminal
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...
/rust#terminal
52 6785 22
New
PragmaticBookshelf
Backend>Learning Resources

Effective Haskell
Build efficient applications that exploit the unique benefits of a pure functional language, learning from an engineer who uses Haskell t...
pragprog.com
#pragprog/haskell#published-book/book-effective-haskell
15 10218 1
New
PragmaticBookshelf
Community>In The Spotlight

Spotlight: Jamis Buck (Author) Interview and AMA!
Author Spotlight Jamis Buck @jamis This month, we have the pleasure of spotlighting author Jamis Buck, who has written Mazes for Prog...
#author-spotlight/ruby/book-the-ray-tracer-challenge/book-mazes-for-programmers
21 6352 9
New
sir.laksmana_wenk
Game Dev>Questions

I want to learn how make a game, but where should I start?
I’m able to do the “artistic” part of game-development; character designing/modeling, music, environment modeling, etc. However, I don’t...
#game-dev
15 4965 9
New
Back to top

Sponsor Spotlight

AppSignal

Catch errors, track performance, monitor hosts and more.

Latest in OCaml

OCaml Portal ❯

Latest in Agda

Agda Portal ❯

Backend>Learning Resources

Backend Learning Resources ❯

Latest on Devtalk

Devtalk ❯

We ❤️ helpful members!

We reward our most helpful members via our MOTM scheme - by giving away a whopping 25 books per year!

Member of the Month

Devtalk Sponsors

Pragmatic Bookshelf

Practical resources that improve the lives of professional developers.

Erlang Solutions

We build trusted fault-tolerant systems that scale to billions of users.

Honeybadger

Real-time error tracking, performance insights, and observability for devs.

EEF

Supporting innovation across the BEAM ecosystem.

coders51

We build reliable cloud platforms for business-critical systems.

Manning Publications

Develop your skills with books, videos, and courses.

AppSignal

Catch errors, track performance, monitor hosts and more.

WyeWorks

Enabling companies to succeed by building software people love.

Pragmatic Studio

Courses that move you from confusion to "Aha, now I get it!"

View all our sponsors ❯

Categories:

Sub Categories:

Popular Portals

Devtalk Sponsors

Pragmatic Bookshelf

Practical resources that improve the lives of professional developers.

Erlang Solutions

We build trusted fault-tolerant systems that scale to billions of users.

Honeybadger

Real-time error tracking, performance insights, and observability for devs.

EEF

Supporting innovation across the BEAM ecosystem.

coders51

We build reliable cloud platforms for business-critical systems.

Manning Publications

Develop your skills with books, videos, and courses.

AppSignal

Catch errors, track performance, monitor hosts and more.

WyeWorks

Enabling companies to succeed by building software people love.

Pragmatic Studio

Courses that move you from confusion to "Aha, now I get it!"

View all our sponsors ❯

We're in Beta

About us Mission Statement See our Roadmap