https://www.minenest.com/437434/ My BROTHER is in DANGER in Minecraft! #aphmau #asheru #cash #dream #habitat #IsInDanger #kidnapped #lodicraft #maizen #Minecraft #MinecraftBut #MinecraftTagalog #MinecraftVideos #nico #pepesantv #PEPSHEYYYN #playofel #sheyyynplayz #tapl #wisp

https://www.minenest.com/429805/ PepeSan turned into a SNAKE in Minecraft! #aphmau #asheru #BecameSnake #cash #dream #habitat #maizen #Minecraft #MinecraftBut #MinecraftTagalog #MinecraftVideos #nico #omocraft #pepesantv #PEPSHEYYYN #playofel #sheyyynplayz #snake #tapl #TurnedSnake #wisp

I'm still fumbling about in the dark with Lean, but my goal for my first big project is to implement system F sub omega and prove its type safety. I'm going to try some simpler lambda calculi first, probably, because I fear that which I do not understand.

Question: Does anyone have tips/examples/guides as to how to start to practically describe a type theory? I started out trying to define evaluation and de Bruijn indices etc and got lost in the weeds. Is there a way to operate fully at a higher level, and only really talk about the types? And if I'm only interested in proving the theory, and not with efficient execution, is there a better way for me to represent scopes/contexts?

#lean #programminglanguagetheory #PLT #proofs #TAPL #Lean4

Et si la théorie vous botte, sachez que Pierce est à l'origine des deux meilleurs livres que j'aie pu lire sur le sujet, d'une pédagogie exceptionnelle :
- Types and Programming Languages #TAPL https://www.cis.upenn.edu/~bcpierce/tapl/
- Advanced Topics in Types and Programming Languages #ATTAPL https://www.cis.upenn.edu/~bcpierce/attapl/index.html

Is there current research on formally verifying “open world” extensible object-oriented code?

For context, I’m reading “EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse” (https://drops.dagstuhl.de/opus/volltexte/2017/7274/pdf/LIPIcs-ECOOP-2017-29.pdf). They use a variation of object algebras which are based on Scott encodings rather than Church encodings to implement PL features modularly, and then do so for all the languages in TAPL. Which is very cool, but raises the question for me: how does one know that the interpreters for the produced languages are correct and their type systems are sound? The visitor approach lets you write side-effect-free code, so headaches around mutability aren’t in play, but I have trouble visualizing how to map a traditional proof like the ones shown in TAPL into a world without algebraic data types.

#FormalVerification #PLT #ProgrammingLanguageTheory #TypeTheory #TAPL #TypesAndProgrammingLanguages #ProofAssistants
#Coq #Isabelle #HOL #Lean4 #Idris #Agda

You can tell that TAPL was written 20 years ago. #TAPL #ProgrammingLanguages #java

Oh no, #TAPL on #ImACeleb

I'm really struggling with TAPL exercise 6.1.4 and there's no solution in the appendix. I can't tell if I'm supposed to build up the set of n-terms inductively using the previous set or build up each n-terms inductively. #TAPL #TypesAndProgrammingLanguages