What are some good AFP entries for beginners? · Beginner Questions

Stream: Beginner Questions

Topic: What are some good AFP entries for beginners?

o7 (Dec 14 2024 at 04:53):

I am looking to improve my understanding of Isabelle/Hol proofs by looking at some simpler articles on the AFP. Are there any examples of these?

Yong Kiam (Dec 16 2024 at 01:08):

are you looking for formalized math or something else?

Yong Kiam (Dec 16 2024 at 01:09):

for the former, maybe some of Manuel Eberl's short entries?

o7 (Dec 16 2024 at 02:17):

I'm looking for single file short entries, but I can take formalised maths too.

Yong Kiam (Dec 16 2024 at 02:19):

https://www.isa-afp.org/authors/eberl/

o7 (Dec 16 2024 at 02:33):

I've skimmed through a few of Manuel's entries, and I think for my level they are a bit too involved for me. I think Tobias's entries are better for me. Thanks for suggesting though.

Yong Kiam (Dec 16 2024 at 02:35):

have you already worked through Concrete semantics?

o7 (Dec 16 2024 at 03:11):

I've read parts of it. Most of the things I've done are from the exercises here https://isabelle.in.tum.de/exercises/index.html which I have found useful due to being more hands-on

Christian Pardillo Laursen (Dec 16 2024 at 10:32):

How about some proofs from THE BOOK? E.g. https://www.isa-afp.org/sessions/irrationals_from_thebook/

o7 (Dec 16 2024 at 11:15):

I haven't seen this one yet. Thanks for showing it to me.

Manuel Eberl (Dec 19 2024 at 19:12):

Last updated: Dec 21 2024 at 16:20 UTC