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

Build Talking Apps for Alexa
For decades, voice-enabled computers have only existed in the realm of science fiction. But now the Alexa Skills Kit (ASK) lets you devel...
pragprog.com
#pragprog#hardware#published-book/book-build-talking-apps-for-alexa
3 3255 0
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

Resourceful Code Reuse
Reusing well-written, well-debugged, and well-tested code improves productivity, code quality, and configurability. It even takes some pr...
pragprog.com
#pragprog#published-book/book-resourceful-code-reuse
3 4093 0
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

Portable Python Projects
Expand your knowledge of the Raspberry Pi while building nearly a dozen immediately applicable hardware and software projects. Use Python...
pragprog.com
#pragprog/python#published-book/book-portable-python-projects
8 3910 2
New
PragmaticBookshelf
Backend>Learning Resources

Python Testing with pytest, Second Edition
Create efficient, elegant software tests in pytest, Python's most powerful testing framework. Brian Okken @brianokken Edited by Kat...
pragprog.com
#pragprog/python#published-book/book-python-testing-with-pytest-second-edition
16 7461 4
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
Backend>Learning Resources

Creating Software with Modern Diagramming Techniques
Communicate more clearly, refactor more effectively, and save time with attractive diagrams that only take minutes to make with open sour...
pragprog.com
#pragprog#published-book#diagrams/book-creating-software-with-modern-diagramming-techniques
6 5316 1
New
PragmaticBookshelf
Backend>Learning Resources

Real-World Event Sourcing
Use event sourcing to solve complex software development problems by modeling your application as a stream of immutable events and their ...
pragprog.com
#pragprog/elixir#published-book/book-real-world-event-sourcing
30 3882 9
New
PragmaticBookshelf
Backend>Learning Resources

Clojure Brain Teasers
Hone your Clojure skills and validate your understanding as you explore the design decisions behind this data-driven functional programmi...
pragprog.com
#pragprog/clojure#published-book/book-clojure-brain-teasers
3 3302 1
New

Other popular topics Top

PragmaticBookshelf
General Dev>Learning Resources

The Pragmatic Programmer, 20th Anniversary Edition
Andy and Dave wrote this influential, classic book to help their clients create better software and rediscover the joy of coding. Almost ...
pragprog.com
#pragprog#published-book/book-the-pragmatic-programmer-20th-anniversary-edition
4 4782 0
New
PragmaticBookshelf
Game Dev>Learning Resources

Apple Game Frameworks and Technologies
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...
pragprog.com
#pragprog#ios#game-dev#macos/swift#published-book#apple/book-apple-game-frameworks-and-technologies
30 7995 10
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
dimitarvp
macOS>Chat

My thoughts on macOS vs Linux
Small essay with thoughts on macOS vs. Linux: I know @Exadra37 is just waiting around the corner to scream at me “I TOLD YOU SO!!!” but I...
#macos#linux
166 9730 69
New
Exadra37
Linux>Questions

What is the most minimalist Linux server distro?
I am asking for any distro that only has the bare-bones to be able to get a shell in the server and then just install the packages as we ...
#linux#servers
66 25846 24
New
AstonJ
Backend>Chat

How to install Ruby 3 with ASDF
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...
/ruby#asdf
11 5961 4
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
AstonJ
AI>Chat

How to: Run DeepSeek on Mac, Windows, and Linux!
This is a very quick guide, you just need to: Download LM Studio: https://lmstudio.ai/ Click on search Type DeepSeek, then select the o...
#macs/deepseek#guides#lm-studio
14 9328 10
New
PragmaticBookshelf
Backend>Learning Resources

Simplicity
Fight complexity and reclaim the original spirit of agility by learning to simplify how you develop software. The result: a more humane a...
pragprog.com
#pragprog#published-book/book-simplicity
10 6553 8
New
xiji2646-netizen
AI>Chat

Claude Code's entire source just leaked (512K lines) - anyone else digging through it?
Woke up to this today: Claude Code’s complete source code exposed via npm source map. Not a snippet. All 512,000 lines. 1,900 TypeScript ...
#claude
6 8359 5
New
Back to top

Sponsor Spotlight

Manning

Develop your skills with books, videos, and courses.

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!"

Linux New Media

Publishing Linux Magazine, ADMIN, and MakerSpace for 25+ years.

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!"

Linux New Media

Publishing Linux Magazine, ADMIN, and MakerSpace for 25+ years.

View all our sponsors ❯

We're in Beta

About us Mission Statement See our Roadmap