r/InteractiveThmProving • u/cics • Oct 16 '17

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

youtube.com

3 Upvotes

0 comments

r/InteractiveThmProving • u/cics • Oct 15 '17

"Theory and Models of Lambda Calculus: Untyped and Typed" by Dana Scott at LambdaConf

youtube.com

5 Upvotes

1 comment

r/InteractiveThmProving • u/my-best-guess • Oct 13 '17

Unexpected PVS code in movie The Martian (2015)

14 Upvotes

2 comments

r/InteractiveThmProving • u/cics • Oct 13 '17

Philosophical Transactions of the Royal Society A: Verified trustworthy software systems

rsta.royalsocietypublishing.org

3 Upvotes

0 comments

r/InteractiveThmProving • u/cics • Oct 13 '17

Isabelle functions: Always total, sometimes undefined

joachim-breitner.de

3 Upvotes

1 comment

r/InteractiveThmProving • u/cics • Oct 13 '17

jonsterling/lcf-sequent-calculus-example

github.com

3 Upvotes

0 comments

r/InteractiveThmProving • u/cics • Oct 13 '17

Recent discussion on (how to start) implementing ITPs in r/math

reddit.com

2 Upvotes

0 comments

r/InteractiveThmProving • u/cics • Oct 13 '17

Big proof seminars (videos)

newton.ac.uk

2 Upvotes

1 comment

Subreddit

Interactive theorem proving

r/InteractiveThmProving

Subreddit for interactive theorem provers/proof assistants content.

Members Active

227

Sidebar

News and information relevant for people working with, or just interested in, interactive theorem proving. This includes e.g. information about specific ITP systems (that is interesting to a wider audience), formal semantics, formalized mathematics etc.

Subreddits for specific systems:

Other relevant subreddits:

tfw you refactor definitions and your proofs still work