The discussion in the post about dependent types is interesting, e.g.: > [...] I'm curious, who has promoted the myth that you need dependent types to do seman

The discussion in the post about dependent types is interesting, e.g.: > [...] I'm curious, who has promoted the myth that you need dependent types to do semantics My experience is that teaching materials for Coq are much more developed in the context of semantics and software verification, despite Coq being harder to use. The post mentions Concrete Semantics [1], which is a really nice Isabelle book. There's also a Lean version [2]. However, to my best knowledge, there's no intermediate/advanced teaching material such as [3-5] for Isabelle, Lean, or Agda. Just introductory stuff. [1] http://www.concrete-semantics.org http://www.concrete-semantics.org [2] https://raw.githubusercontent.com/blanchette/logical_verification_2020/master/hitchhikers_guide.pdf https://raw.githubusercontent.com/blanchette/logical_verific... [3] http://adam.chlipala.net/frap http://adam.chlipala.net/frap [4] http://adam.chlipala.net/cpdt http://adam.chlipala.net/cpdt [5] https://ilyasergey.net/pnp https://ilyasergey.net/pnp