| | Introduction to the λ-Calculus (lawrencecpaulson.github.io) |
|
46 points by matt_d 86 days ago | past | 19 comments
|
|
| | Two Small Examples by Fields Medallists (lawrencecpaulson.github.io) |
|
2 points by zaik 10 months ago | past
|
|
| | Propositions as Types: Explained (and Debunked) (lawrencecpaulson.github.io) |
|
4 points by hackandthink 11 months ago | past | 1 comment
|
|
| | What do we mean by "the foundations of mathematics"? (lawrencecpaulson.github.io) |
|
139 points by JoelMcCracken on Nov 1, 2023 | past | 139 comments
|
|
| | The concept of proof within the context of machine mathematics (lawrencecpaulson.github.io) |
|
2 points by chmaynard on Oct 4, 2023 | past
|
|
| | Lambda Calculus: Some Models, Some Philosophy [pdf] (lawrencecpaulson.github.io) |
|
4 points by 082349872349872 on Aug 31, 2023 | past | 1 comment
|
|
| | Types versus sets (and what about categories?) (2022) (lawrencecpaulson.github.io) |
|
101 points by matt_d on Aug 31, 2023 | past | 36 comments
|
|
| | Propositions as Types: Explained (and Debunked) (lawrencecpaulson.github.io) |
|
3 points by ykonstant on Aug 23, 2023 | past
|
|
| | When is a computer proof a proof? (lawrencecpaulson.github.io) |
|
2 points by furcyd on Aug 9, 2023 | past
|
|
| | The ALEXANDRIA Project: What has been accomplished? (lawrencecpaulson.github.io) |
|
2 points by vilhelm_s on April 27, 2023 | past
|
|
| | The semantics of a simple functional language (lawrencecpaulson.github.io) |
|
96 points by matt_d on March 11, 2023 | past | 6 comments
|
|
| | Formalising a new proof that the square root of two is irrational (lawrencecpaulson.github.io) |
|
103 points by ColinWright on Jan 19, 2023 | past | 86 comments
|
|
| | Memories: Artificial Intelligence at Stanford in the 70s (lawrencecpaulson.github.io) |
|
72 points by furcyd on Jan 11, 2023 | past | 14 comments
|
|
| | Thoughts on user interfaces for theorem provers (lawrencecpaulson.github.io) |
|
3 points by todsacerdoti on Dec 19, 2022 | past | 3 comments
|
|
| | Memories: First exposure to computers (lawrencecpaulson.github.io) |
|
70 points by furcyd on Dec 7, 2022 | past | 56 comments
|
|
| | Verifying distributed systems with Isabelle/HOL (lawrencecpaulson.github.io) |
|
163 points by eatonphil on Oct 12, 2022 | past | 18 comments
|
|
| | Memories: Edinburgh ML to Standard ML (lawrencecpaulson.github.io) |
|
119 points by todsacerdoti on Oct 5, 2022 | past | 40 comments
|
|
| | Proving the Obvious (lawrencecpaulson.github.io) |
|
2 points by todsacerdoti on Sept 19, 2022 | past
|
|
| | Why are you being constructive? (lawrencecpaulson.github.io) |
|
1 point by todsacerdoti on Sept 18, 2022 | past
|
|
| | Ackermann's function is not primitive recursive, I (lawrencecpaulson.github.io) |
|
2 points by furcyd on Aug 31, 2022 | past
|
|
| | On Turing Machines (lawrencecpaulson.github.io) |
|
1 point by signa11 on Aug 6, 2022 | past
|
|
| | On Turing Machines (lawrencecpaulson.github.io) |
|
26 points by furcyd on July 6, 2022 | past | 3 comments
|
|
| | What is the point of formalising mathematics? (lawrencecpaulson.github.io) |
|
1 point by nabla9 on June 22, 2022 | past
|
|
| | What is the point of formalising mathematics? (lawrencecpaulson.github.io) |
|
5 points by furcyd on June 22, 2022 | past
|
|
| | Formalising Gödel's incompleteness theorems, I (lawrencecpaulson.github.io) |
|
83 points by furcyd on May 18, 2022 | past | 51 comments
|
|
| | Types versus sets (and what about categories?) (lawrencecpaulson.github.io) |
|
79 points by carnitine on March 16, 2022 | past | 31 comments
|
|
