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 1251 0

Where Next?

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

Popular Backend topics Top

PragmaticBookshelf
Backend>Learning Resources

Complex Network Analysis in Python
Construct, analyze, and visualize networks with networkx, a Python language module. Discover how to work with social, product, temporal, ...
pragprog.com
#pragprog/python#published-book/book-complex-network-analysis-in-python
4 2049 1
New
PragmaticBookshelf
Backend>Learning Resources

Modern C++ Programming with Test-Driven Development
Modern C++ Programming With Test-Driven Development, the only comprehensive treatment on TDD in C++ provides you with everything you need...
pragprog.com
#pragprog/c-plus-plus#published-book/book-modern-c-programming-with-test-driven-development
2 1653 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 2081 2
New
PragmaticBookshelf
Backend>Learning Resources

Go Brain Teasers
Miki Tebeka @tebeka edited by Margaret Eldridge @Margaret This book contains 25 simple Go programs and will challenge your understanding...
pragprog.com
#pragprog/go#published-book/book-go-brain-teasers
12 1707 4
New
PragmaticBookshelf
Backend>Learning Resources

Learn to Program, Third Edition
It's easier to learn how to program a computer than it has ever been before. Now everyone can learn to write programs for themselves—no p...
pragprog.com
#pragprog/ruby#published-book/book-learn-to-program-third-edition
11 2451 5
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 4119 24
New
ManningBooks
Backend>Learning Resources

Kubernetes in Action, Second Edition
Kubernetes in Action, Second Edition teaches you to use Kubernetes to deploy container-based distributed applications. You'll start with ...
manning.com
#manning#kubernetes#meap
4 1844 0
New
PragmaticBookshelf
Backend>Learning Resources

Ruby on Rails Background Jobs with Sidekiq
Give your Rail's apps an instant performance boost by harnessing the power of efficient, manageable, and sustainable background processin...
pragprog.com
#pragprog/ruby/rails#published-book/book-ruby-on-rails-background-jobs-with-sidekiq
2 1823 0
New
PragmaticBookshelf
Backend>Learning Resources

Engineering Elixir Applications
Develop, deploy, and debug BEAM applications using BEAMOps: a new paradigm that focuses on scalability, fault tolerance, and owning each ...
pragprog.com
#pragprog/elixir#published-book/book-engineering-elixir-applications
40 2292 21
New
PragmaticBookshelf
Backend>Learning Resources

MySQL 9 Essentials
A concise guide to MySQL 9 database administration, covering fundamental concepts, techniques, and best practices. Neil Smyth MySQL...
pragprog.com
#pragprog#published-book/mysql/book-mysql-9-essentials
2 836 0
New

Other popular topics Top

AstonJ
General Dev>Dev Chat

Which language or framework do you want to learn next?
Curious to know which languages and frameworks you’re all thinking about learning next :upside_down_face: Perhaps if there’s enough peop...
#community#learning
243 5922 95
New
AstonJ
General Dev>Hardware

Custom keyboard keycaps
There’s a whole world of custom keycaps out there that I didn’t know existed! Check out all of our Keycaps threads here: https://forum....
#hardware/keyboards#keycaps#mechanical-keyboards
15 8183 19
New
Exadra37
macOS>Chat

Your Mac Isn't Yours - worse, it spies on you and sends it home unencrypted
On modern versions of macOS, you simply can’t power on your computer, launch a text editor or eBook reader, and write or read, without a ...
sneak.berlin
#macos#macs#big-sur#apple#privacy#mac-privacy
24 3679 24
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 6920 31
New
Margaret
General Dev>Content Creators

What tech topics do you think will (or should) be the focus of 2021?
Hello content creators! Happy new year. What tech topics do you think will be the focus of 2021? My vote for one topic is ethics in tech...
#general
110 3900 43
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 21694 24
New
PragmaticBookshelf
Community>In The Spotlight

Spotlight: Paolo Perrotta (Author)
“A Mystical Experience” Hero’s Journey with Paolo Perrotta @nusco Ever wonder how authoring books compares to writing articles?...
#community#author-spotlight/book-programming-machine-learning/book-metaprogramming-ruby-2
31 3538 15
New
AstonJ
General Dev>Dev Chat

Languages Without Garbage Collection
Continuing the discussion from Thinking about learning Crystal, let’s discuss - I was wondering which languages don’t GC - maybe we can c...
#garbage-collection
21 4800 7
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 5598 9
New
Help
Game Dev>Questions

Can I use Java to program a game for Nintendo switch?
I am trying to crate a game for the Nintendo switch, I wanted to use Java as I am comfortable with that programming language. Can you use...
/java#nintendo
8 3528 3
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.

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'll 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.

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'll 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