[HN Gopher] The semantics of a simple functional language
       ___________________________________________________________________
        
       The semantics of a simple functional language
        
       Author : matt_d
       Score  : 61 points
       Date   : 2023-03-11 07:45 UTC (1 days ago)
        
 (HTM) web link (lawrencecpaulson.github.io)
 (TXT) w3m dump (lawrencecpaulson.github.io)
        
       | nextos wrote:
       | 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
       | 
       | [2]
       | https://raw.githubusercontent.com/blanchette/logical_verific...
       | 
       | [3] http://adam.chlipala.net/frap
       | 
       | [4] http://adam.chlipala.net/cpdt
       | 
       | [5] https://ilyasergey.net/pnp
        
       | gergo_barany wrote:
       | This started a bit of a competition, some other versions of the
       | same proofs in Agda and Lean are linked from here:
       | https://mastodon.online/@nomeata/110004145921681756
        
       ___________________________________________________________________
       (page generated 2023-03-12 23:01 UTC)