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

Programming Phoenix 1.4
Don’t accept the compromise between fast and beautiful: you can have it all. Phoenix creator Chris McCord, Elixir creator José Valim, and...
pragprog.com
#pragprog/elixir/phoenix#published-book/book-programming-phoenix-1-4
16 3402 3
New
PragmaticBookshelf
Backend>Learning Resources

Programming Clojure, Third Edition
Drowning in unnecessary complexity, unmanaged state, and tangles of spaghetti code? Clojure cuts through complexity by providing a set of...
pragprog.com
#pragprog/clojure#published-book/book-programming-clojure-third-edition
4 3644 0
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

Mockito Made Clear
Write effective and useful tests with the Mockito framework. Distinguish between mocks, stubs, and spies, and feel confident about when a...
pragprog.com
#pragprog/java#published-book/book-mockito-made-clear
4 3476 0
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

Pragmatic Unit Testing in Java with JUnit, Third Edition
Done poorly, unit testing wastes your time and degrades your code. So pick up the third edition of this book and see how to test properly...
pragprog.com
#pragprog/java#published-book/book-pragmatic-unit-testing-in-java-with-junit-third-edition
2 3284 0
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
PragmaticBookshelf
Backend>Learning Resources

Build, Tune, Explore with OpenWebRX+
Build a web-connected software-defined receiver with OpenWebRX+ software, a Raspberry Pi, and an RTL-SDR USB stick. Explore and share the...
pragprog.com
#hardware
2 3002 1
New
PragmaticBookshelf
Backend>Learning Resources

Haskell Brain Teasers
Deepen your Haskell knowledge, sharpen your functional programming skills, and just have fun with 20 functional programming puzzles to ti...
pragprog.com
#pragprog
3 1520 1
New

Other popular topics Top

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>Dev Chat

How fast do you type? Check your WPM here!
Do the test and post your score :nerd_face: :keyboard: If possible, please add info such as the keyboard you’re using, the layout (Qw...
typing-speed-test.aoeu.eu
/keyboards
82 7682 31
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
General Dev>Code Editors

Doom-Emacs: Can't find emacs in your PATH
If you get Can't find emacs in your PATH when trying to install Doom Emacs on your Mac you… just… need to install Emacs first! :lol: bre...
#macos/emacs#doom-emacs
4 5837 0
New
PragmaticBookshelf
Community>In The Spotlight

Spotlight: Peter Ullrich (Author) Interview and AMA!
Author Spotlight: Peter Ullrich @PJUllrich Data is at the core of every business, but it is useless if nobody can access and analyze ...
/elixir/phoenix/book-building-table-views-with-phoenix-liveview
72 4765 21
New
PragmaticBookshelf
Community>In The Spotlight

Spotlight: Bruce Tate (Author) Interview and AMA!
Author Spotlight: Bruce Tate @redrapids Programming languages always emerge out of need, and if that’s not always true, they’re defin...
/elixir/ruby/phoenix/book-seven-more-languages-in-seven-weeks/book-seven-languages-in-seven-weeks#liveview/book-programming-phoenix-liveview
54 5678 23
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
PragmaticBookshelf
Backend>Learning Resources

Agile Web Development with Rails 8
Get the comprehensive, insider information you need for Rails 8 with the new edition of this award-winning classic. Sam Ruby @rubys ...
pragprog.com
#pragprog#web-development/ruby/rails#published-book/book-agile-web-development-with-rails-8
12 7404 7
New
AstonJ
AI>In The News

DeepSeek (671B) running on a cluster of 8 Mac Mini Pros with 64GB RAM each
This is cool! DEEPSEEK-V3 ON M4 MAC: BLAZING FAST INFERENCE ON APPLE SILICON We just witnessed something incredible: the largest open-s...
#ai#macs/deepseek
0 6695 1
New
PragmaticBookshelf
Backend>Learning Resources

Advanced Functional Programming with Elixir
Use advanced functional programming principles, practical Domain-Driven Design techniques, and production-ready Elixir code to build scal...
joekoski.com
#pragprog/elixir#published-book#functional-programming/book-advanced-functional-programming-with-elixir
43 4989 22
New
Back to top

Sponsor Spotlight

Erlang Solutions

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

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