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 Chatbot Interactions
The next step in the evolution of user interfaces is here. Chatbots let your users interact with your service in their own natural langua...
pragprog.com
#pragprog/ruby#published-book/book-build-chatbot-interactions
12 3546 6
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

Learn Functional Programming with Elixir
Elixir's straightforward syntax and this guided tour give you a clean, simple path to learn modern functional programming techniques. Exp...
pragprog.com
#pragprog/elixir#published-book/book-learn-functional-programming-with-elixir
11 3267 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

Domain Modeling Made Functional
You want increased customer satisfaction, faster development cycles, and less wasted work. Domain-driven design (DDD) and functional prog...
pragprog.com
#pragprog#published-book/book-domain-modeling-made-functional
19 4664 9
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 Phoenix LiveView
Build highly interactive applications without ever leaving Elixir, the way the experts do. Let LiveView take care of performance, scalabi...
pragprog.com
#pragprog/elixir/phoenix#published-book/book-programming-phoenix-liveview
83 11955 26
New
PragmaticBookshelf
Backend>Learning Resources

Programming WebRTC
Use WebRTC to build web applications that stream media and data in real time directly from one user to another, all in the browser. ...
pragprog.com
#pragprog#published-book/js#webrtc/book-programming-webrtc
27 6969 6
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

Risk-First Software Development, Second Edition
As digital systems increasingly run the world, mastery of the recurring patterns of software development risk is the key to fast and effe...
pragprog.com
#pragprog#published-book/book-risk-first-software-development-second-edition
12 4217 8
New

Other popular topics Top

PragmaticBookshelf
Backend>Learning Resources

Testing Elixir
Write Elixir tests that you can be proud of. Dive into Elixir’s test philosophy and gain mastery over the terminology and concepts that u...
pragprog.com
#pragprog/elixir#published-book/book-testing-elixir
33 5004 8
New
AstonJ
Science/Tech>Tech Chat

What are you watching?
Or looking forward to? :nerd_face:
#community
498 14002 274
New
AstonJ
Data Science

Can AI/ML predict a lottery win?
Biggest jackpot ever apparently! :upside_down_face: I don’t (usually) gamble/play the lottery, but working on a program to predict the...
#ai#machine-learning
19 3939 10
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
AstonJ
Science/Tech>Health & Diet

David Sinclair's new Lifespan podcast
We’ve talked about his book briefly here but it is quickly becoming obsolete - so he’s decided to create a series of 7 podcasts, the firs...
#health#podcasts#bio-hackers#david-sinclair
87 6790 49
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
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
AnfaengerAlex
Android>Questions

Unresolved Reference to android in build.gradle.kts – Beginner Issue
Hello, I’m a beginner in Android development and I’m facing an issue with my project setup. In my build.gradle.kts file, I have the foll...
#binding
0 7460 2
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
RobertRichards
Game Dev>Chat

Hair Salon Games for Girls Fun
Hair Salon Games for Girls Fun Girls Hair Saloon game is mainly developed for kids. This game allows users to select virtual avatars to ...
#ios#android#unity#fun
2 3556 1
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