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

Agile Web Development with Rails 6
Ruby on Rails helps you produce high-quality, beautiful-looking web applications quickly—you concentrate on creating the application, and...
pragprog.com
#pragprog#web-development/ruby/rails#published-book/book-agile-web-development-with-rails-6
4 4454 0
New
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 3825 1
New
PragmaticBookshelf
Backend>Learning Resources

Learn to Program (2nd edition)
For this new edition of the best-selling Learn to Program, Chris Pine has taken a good thing and made it even better. First, he used the ...
pragprog.com
#pragprog/ruby#published-book/book-learn-to-program-2nd-edition
10 3737 6
New
PragmaticBookshelf
Backend>Learning Resources

SQL Antipatterns, Volume 1
SQL Antipatterns is a short-cut to wisdom, showing you how to avoid "easy" solutions that don't work, and be a better database developer ...
pragprog.com
#pragprog#published-book#data-science/book-sql-antipatterns-volume-1
27 3918 4
New
PragmaticBookshelf
Backend>Learning Resources

Machine Learning in Elixir
Leverage Elixir and the Nx ecosystem to build intelligent applications that solve real-world problems in computer vision, natural languag...
pragprog.com
#pragprog/elixir#published-book#machine-learning#nx/book-machine-learning-in-elixir
18 4615 7
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
PragmaticBookshelf
Backend>Learning Resources

Automate Your Home Using Go
Dive into extraordinary and robust home automation projects written in Go. Deploy, host, and maintain code in your home lab using best of...
pragprog.com
#pragprog/go#published-book/book-automate-your-home-using-go
3 3146 1
New
PragmaticBookshelf
Backend>Learning Resources

Server-Driven Web Apps with htmx
Build modern server-driven web applications using htmx. Whatever programming language you use, you’ll write less (and cleaner) code. ...
pragprog.com
#pragprog#web-development#published-book/book-server-driven-web-apps-with-htmx
6 5257 3
New
PragmaticBookshelf
Backend>Learning Resources

Next-Level A/B Testing
Take your experimentation strategy to the next level so you can effectively understand the impact of changes to user, product, and busine...
pragprog.com
#pragprog#published-book#testing/book-next-level-a-b-testing
2 4809 1
New
PragmaticBookshelf
Backend>Learning Resources

C# Brain Teasers
Test your C# knowledge and expand your understanding of the language with 25 common and not-so-common puzzles. Steve Love @stevelov...
pragprog.com
#pragprog#published-book/book-c-sharp-brain-teasers
2 3349 1
New

Other popular topics Top

DevotionGeo
Backend>Questions

Can someone explain the -t option/flag in docker run command?
I know that -t flag is used along with -i flag for getting an interactive shell. But I cannot digest what the man page for docker run com...
#docker
7 10261 2
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
Backend>Questions

Erlang's not installing on macOS Big Sur "You are natively building Erlang/OTP for a later version of MacOSX than current version"
Just done a fresh install of macOS Big Sur and on installing Erlang I am getting: asdf install erlang 23.1.2 Configure failed. checking ...
#macos/erlang#big-sur#asdf
10 6212 8
New
Exadra37
Linux>Chat

RancherOS is in end of life
Oh just spent so much time on this to discover now that RancherOS is in end of life but Rancher is refusing to mark the Github repo as su...
#linux#rancheros
10 6358 6
New
mafinar
Backend>Chat

Data Structures and Algorithms with Elixir
This is going to be a long an frequently posted thread. While talking to a friend of mine who has taken data structure and algorithm cou...
/elixir#algorithms#data-structures
108 11869 31
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>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

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 4162 0
New
PragmaticBookshelf
General Dev>Learning Resources

Write Better with Vale
Lint your docs like code: turn any style guide into enforceable rules with Vale and publish clear, consistent content every time. ...
pragprog.com
#pragprog#published-book#vale/book-write-better-with-vale
8 9973 5
New
pragdave
AI>Learning Resources

A Common-Sense Guide to AI Engineering
Build robust LLM-powered apps, chatbots, and agents while mastering AI engineering principles that will help you outlast the tools and th...
pragprog.com
#pragprog
17 1852 8
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