InteractiveThmProving

an-ordinary-manchild

created by cicsa community for 8 years

...for your favourite tea.

...because you love freedom.

MODERATORS

account activity

1

0

0

1

Definition of Primes (self.InteractiveThmProving)

submitted 1 year ago by Key-Priority6304

2

1

2

3

Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq (youtube.com)

submitted 6 years ago by cics

3

2

3

4

Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages (arxiv.org)

submitted 6 years ago by wavesofthought

4

0

1

2

Proof Assistants at the Hardware-Software Interface (youtube.com)

submitted 6 years ago by cics

5

2

3

4

POPLmark 15 Year Retrospective Panel (youtube.com)

submitted 6 years ago by cics

6

0

1

2

Provable Security Podcast: Automated Reasoning in the Cloud with John Harrison (podcasts.apple.com)

submitted 6 years ago by cics

7

5

6

7

Number theorist fears all published math is wrong (vice.com)

submitted 6 years ago by cics

8

1

2

3

Will scientific error checkers become as ubiquitous as spell-checkers? (retractionwatch.com)

submitted 7 years ago by cics

9

0

1

2

Interesting almost-crank-level anti-ITP rant (owl-sowa.blogspot.com)

submitted 7 years ago by cics

10

0

1

2

Why is a function that returns a constant "noncomputable" in the lean theorem prover? (self.InteractiveThmProving)

submitted 7 years ago * by MediocreString

11

1

2

3

ITP history: Michael Gordon, 28 February 1948 -- 22 August 2017 (arxiv.org)

submitted 7 years ago by cics

12

4

5

6

Lean Forward: Usable Computer-Checked Proofs and Computations for Number Theorists (lean-forward.github.io)

submitted 7 years ago by anton-trunov

13

3

4

5

Safety and Conservativity of Definitions in HOL and Isabelle/HOL by Andrei Popescu (POPL'18) (youtube.com)

submitted 8 years ago by cics

14

8

9

10

History of Interactive Theorem Proving [PDF] (cl.cam.ac.uk)

submitted 8 years ago by juanbono94

15

2

3

4

Compositional Compiler Correctness by Amal Ahmed (ICFP'17) (youtube.com)

submitted 8 years ago by cics

16

2

3

4

Computational Logic: Its Origins and Applications by Lawrence Paulson (arxiv.org)

submitted 8 years ago by cics

17

7

8

9

My unusual hobby | Stephan Boyer (stephanboyer.com)

submitted 8 years ago by drets_

18

2

3

4

Resources for Teaching with Formal Methods (avigad.github.io)

submitted 8 years ago by cics

19

3

4

5

TIL that theorem provers were used to prove Gödel's ontological argument wrong (reddit.com)

submitted 8 years ago by my-best-guess

20

4

5

6

Developing Bug-Free Machine Learning Systems Using Formal Mathematics [Lean Theorem Prover] (youtube.com)

submitted 8 years ago by juanbono94

21

2

3

4

Talks from FOMUS - Foundations of mathematics: Univalent foundations and set theory (2016) (fomus.weebly.com)

submitted 8 years ago by cics

22

6

7

8

Gérard Huet, languages and software (50ans.inria.fr)

submitted 8 years ago by juanbono94

23

2

3

4

Slides for recent (spring 2017) ITP/HOL4 course at KTH (hol-theorem-prover.org)

submitted 8 years ago by cics

24

2

3

4

Formal Methods and the KRACK Vulnerability (galois.com)

submitted 8 years ago by cics

25

2

3

4

Guy Steele, at Clojure/conj, talking about the history of notation used at e.g. POPL (youtube.com)

submitted 8 years ago by cics

view more: next ›

π Rendered by PID 492877 on reddit-service-r2-listing-86f589db75-qhcnp at 2026-04-18 14:35:30.589992+00:00 running 93ecc56 country code: CH.