#ProgrammingLanguageTheory

Jan de Muijnck-Hughes*Last Call* I have a <a href="https://discuss.systems/tags/PhD" class="mention hashtag" rel="nofollow noopener" target="_blank">#PhD</a> position for UK students, available with myself and <a href="https://types.pl/@bentnib" class="u-url mention" rel="nofollow noopener" target="_blank">@bentnib</a> This project will be looking at developing new methods for asserting the resilience of existing communicating systems by developing new static analysis methods derived from advanced programming language research.*Hard Deadline*: Wednesday 16th April 2025You will belong to <a href="https://mastodon.acm.org/@StrathCyber" class="u-url mention" rel="nofollow noopener" target="_blank">@StrathCyber</a> and <a href="https://mastodon.acm.org/@mspstrath" class="u-url mention" rel="nofollow noopener" target="_blank">@mspstrath</a>, as well as gaining access to <a href="https://mastodon.scot/@spli" class="u-url mention" rel="nofollow noopener" target="_blank">@spli</a> <a href="https://www.strath.ac.uk/studywithus/postgraduateresearchphdopportunities/science/computerinformationsciences/towardstype-drivenassuranceofcommunicatingsystems/" rel="nofollow noopener" translate="no" target="_blank">https://www.strath.ac.uk/studywithus/postgraduateresearchphdopportunities/science/computerinformationsciences/towardstype-drivenassuranceofcommunicatingsystems/</a>(Ignore the deadline on the advert)Please spread the words. <a href="https://discuss.systems/tags/dependentTypes" class="mention hashtag" rel="nofollow noopener" target="_blank">#dependentTypes</a> <a href="https://discuss.systems/tags/formalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#formalMethods</a> <a href="https://discuss.systems/tags/idris" class="mention hashtag" rel="nofollow noopener" target="_blank">#idris</a> <a href="https://discuss.systems/tags/programmingLanguageTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#programmingLanguageTheory</a> <a href="https://discuss.systems/tags/typeTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#typeTheory</a> <a href="https://discuss.systems/tags/idris2" class="mention hashtag" rel="nofollow noopener" target="_blank">#idris2</a> <a href="https://discuss.systems/tags/computerSecurity" class="mention hashtag" rel="nofollow noopener" target="_blank">#computerSecurity</a> <a href="https://discuss.systems/tags/cybersecurity" class="mention hashtag" rel="nofollow noopener" target="_blank">#cybersecurity</a> <a href="https://discuss.systems/tags/securityByDesign" class="mention hashtag" rel="nofollow noopener" target="_blank">#securityByDesign</a> <a href="https://discuss.systems/tags/secureByDesign" class="mention hashtag" rel="nofollow noopener" target="_blank">#secureByDesign</a>

jnkrtechI'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?<a href="https://social.treehouse.systems/tags/lean" class="mention hashtag" rel="nofollow noopener" target="_blank">#lean</a> <a href="https://social.treehouse.systems/tags/programminglanguagetheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#programminglanguagetheory</a> <a href="https://social.treehouse.systems/tags/PLT" class="mention hashtag" rel="nofollow noopener" target="_blank">#PLT</a> <a href="https://social.treehouse.systems/tags/proofs" class="mention hashtag" rel="nofollow noopener" target="_blank">#proofs</a> <a href="https://social.treehouse.systems/tags/TAPL" class="mention hashtag" rel="nofollow noopener" target="_blank">#TAPL</a> <a href="https://social.treehouse.systems/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#Lean4</a>

Jan de Muijnck-HughesI have a funded <a href="https://discuss.systems/tags/PhD" class="mention hashtag" rel="nofollow noopener" target="_blank">#PhD</a> position for UK students, available with myself and <a href="https://types.pl/@bentnib" class="u-url mention" rel="nofollow noopener" target="_blank">@bentnib</a> This project will be looking at developing new methods for asserting the resilience of existing communicating systems by developing new static analysis methods derived from advanced programming language research.Deadline: Thursday 20th March 2025You will belong to <a href="https://mastodon.acm.org/@StrathCyber" class="u-url mention" rel="nofollow noopener" target="_blank">@StrathCyber</a> and <a href="https://mastodon.acm.org/@mspstrath" class="u-url mention" rel="nofollow noopener" target="_blank">@mspstrath</a>, as well as gaining access to <a href="https://mastodon.scot/@spli" class="u-url mention" rel="nofollow noopener" target="_blank">@spli</a> For now more details about the project are on my personal website.<a href="https://tyde.systems/page/position/2025-jarss/" rel="nofollow noopener" translate="no" target="_blank">https://tyde.systems/page/position/2025-jarss/</a>Please spread the words. <a href="https://discuss.systems/tags/dependentTypes" class="mention hashtag" rel="nofollow noopener" target="_blank">#dependentTypes</a> <a href="https://discuss.systems/tags/formalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#formalMethods</a> <a href="https://discuss.systems/tags/idris" class="mention hashtag" rel="nofollow noopener" target="_blank">#idris</a> <a href="https://discuss.systems/tags/programmingLanguageTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#programmingLanguageTheory</a> <a href="https://discuss.systems/tags/typeTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#typeTheory</a> <a href="https://discuss.systems/tags/idris2" class="mention hashtag" rel="nofollow noopener" target="_blank">#idris2</a> <a href="https://discuss.systems/tags/computerSecurity" class="mention hashtag" rel="nofollow noopener" target="_blank">#computerSecurity</a> <a href="https://discuss.systems/tags/cybersecurity" class="mention hashtag" rel="nofollow noopener" target="_blank">#cybersecurity</a> <a href="https://discuss.systems/tags/securityByDesign" class="mention hashtag" rel="nofollow noopener" target="_blank">#securityByDesign</a> <a href="https://discuss.systems/tags/secureByDesign" class="mention hashtag" rel="nofollow noopener" target="_blank">#secureByDesign</a>

b4ux1t3 :trek_ds9_sisko:#1️⃣Just got paid to write a formal grammar.Does this make me a professional language writer?<a href="https://hachyderm.io/tags/Programming" class="mention hashtag" rel="nofollow noopener" target="_blank">#Programming</a> <a href="https://hachyderm.io/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#ProgrammingLanguageTheory</a>

MaciekType checking approach to estimating sensitivity bounds in differential privacy: Gradual Differentially Private Programming - <a href="https://cacm.acm.org/latin-america-regional-special-section/gradual-differentially-private-programming/" rel="nofollow noopener" translate="no" target="_blank">https://cacm.acm.org/latin-america-regional-special-section/gradual-differentially-private-programming/</a><a href="https://hachyderm.io/tags/DifferentialPrivacy" class="mention hashtag" rel="nofollow noopener" target="_blank">#DifferentialPrivacy</a> <a href="https://hachyderm.io/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#ProgrammingLanguageTheory</a>

DocRekd<a href="https://pony.social/@thephd" class="u-url mention" rel="nofollow noopener" target="_blank">@thephd</a> <a href="https://cloudisland.nz/@ehashman" class="u-url mention" rel="nofollow noopener" target="_blank">@ehashman</a> Ok but tbf <a href="https://hachyderm.io/tags/goLang" class="mention hashtag" rel="nofollow noopener" target="_blank">#goLang</a> ignored the previous 50 years of <a href="https://hachyderm.io/tags/programmingLanguageTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#programmingLanguageTheory</a>, confirming that Rob Pike and Ken Thompson cannot design a <a href="https://hachyderm.io/tags/programmingLanguage" class="mention hashtag" rel="nofollow noopener" target="_blank">#programmingLanguage</a> to save their life, instead making a worse <a href="https://hachyderm.io/tags/javeLang" class="mention hashtag" rel="nofollow noopener" target="_blank">#javeLang</a>Even <a href="https://hachyderm.io/tags/Rust" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rust</a> can do a map a Vec and return another Vec in a one-liner

peraNext Wednesday I will be visiting St Andrews for the first Scottish Programming Languages Seminar of 2024. The program looks pretty interesting: <a href="https://scottish-pl-institute.github.io/spls/meetings/2024/march/" rel="nofollow noopener" translate="no" target="_blank">https://scottish-pl-institute.github.io/spls/meetings/2024/march/</a> <a href="https://mastodon.social/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#ProgrammingLanguageTheory</a> <a href="https://mastodon.social/tags/PLT" class="mention hashtag" rel="nofollow noopener" target="_blank">#PLT</a>

रञ्जित (Ranjit Mathew)An interesting resource for learning <a href="https://mastodon.social/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#TypeTheory</a> and adjacent areas like <a href="https://mastodon.social/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#CategoryTheory</a>:“learn-tt”, Daniel Gratzer (<a href="https://github.com/jozefg/learn-tt" rel="nofollow noopener" translate="no" target="_blank">https://github.com/jozefg/learn-tt</a>).<a href="https://mastodon.social/tags/Types" class="mention hashtag" rel="nofollow noopener" target="_blank">#Types</a> <a href="https://mastodon.social/tags/PLT" class="mention hashtag" rel="nofollow noopener" target="_blank">#PLT</a> <a href="https://mastodon.social/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#ProgrammingLanguageTheory</a> <a href="https://mastodon.social/tags/PLDI" class="mention hashtag" rel="nofollow noopener" target="_blank">#PLDI</a>

fanf42<a href="https://social.treehouse.systems/@jnkrtech" class="u-url mention" rel="nofollow noopener" target="_blank">@jnkrtech</a> <a href="https://social.treehouse.systems/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://social.treehouse.systems/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#TypeTheory</a> <a href="https://social.treehouse.systems/tags/Scala" class="mention hashtag" rel="nofollow noopener" target="_blank">#Scala</a> <a href="https://social.treehouse.systems/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#ProgrammingLanguageTheory</a> <a href="https://social.treehouse.systems/tags/plt" class="mention hashtag" rel="nofollow noopener" target="_blank">#plt</a> o thing it is but iirc there was subtleties. Yes scala is the only one, generally language either choose a way without object at all (Haskell, coq...) or model object/higher kind differently (ocaml). Why so? Because is absurdly hard, comes with bad consequences (type inference is not good), and the power at hand is rarely necessary (remember that most of the industry things js, python c and Java are good enough)

jnkrtechA few questions that have been nagging me:- Is Scala’s theory of dependent objects a generalization of system f sub omega? - If so, is Scala the only mainstream language that implements f sub omega? - Why does f sub omega seem to be so rare in mainstream languages, when in the abstract it sounds like it would be the most powerful?<a href="https://social.treehouse.systems/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://social.treehouse.systems/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#TypeTheory</a> <a href="https://social.treehouse.systems/tags/Scala" class="mention hashtag" rel="nofollow noopener" target="_blank">#Scala</a> <a href="https://social.treehouse.systems/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#ProgrammingLanguageTheory</a> <a href="https://social.treehouse.systems/tags/plt" class="mention hashtag" rel="nofollow noopener" target="_blank">#plt</a>

jnkrtechIs 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” (<a href="https://drops.dagstuhl.de/opus/volltexte/2017/7274/pdf/LIPIcs-ECOOP-2017-29.pdf" rel="nofollow noopener" translate="no" target="_blank">https://drops.dagstuhl.de/opus/volltexte/2017/7274/pdf/LIPIcs-ECOOP-2017-29.pdf</a>). 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.<a href="https://social.treehouse.systems/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#FormalVerification</a> <a href="https://social.treehouse.systems/tags/PLT" class="mention hashtag" rel="nofollow noopener" target="_blank">#PLT</a> <a href="https://social.treehouse.systems/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#ProgrammingLanguageTheory</a> <a href="https://social.treehouse.systems/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#TypeTheory</a> <a href="https://social.treehouse.systems/tags/TAPL" class="mention hashtag" rel="nofollow noopener" target="_blank">#TAPL</a> <a href="https://social.treehouse.systems/tags/TypesAndProgrammingLanguages" class="mention hashtag" rel="nofollow noopener" target="_blank">#TypesAndProgrammingLanguages</a> <a href="https://social.treehouse.systems/tags/ProofAssistants" class="mention hashtag" rel="nofollow noopener" target="_blank">#ProofAssistants</a> <a href="https://social.treehouse.systems/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://social.treehouse.systems/tags/Isabelle" class="mention hashtag" rel="nofollow noopener" target="_blank">#Isabelle</a> <a href="https://social.treehouse.systems/tags/HOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#HOL</a> <a href="https://social.treehouse.systems/tags/Lean4" class="mention hashtag" rel="nofollow noopener" target="_blank">#Lean4</a> <a href="https://social.treehouse.systems/tags/Idris" class="mention hashtag" rel="nofollow noopener" target="_blank">#Idris</a> <a href="https://social.treehouse.systems/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a>

FissionThis week, we hosted a fascinating discussion with <a href="https://merveilles.town/@nasser" class="u-url mention" rel="nofollow noopener" target="_blank">@nasser</a> and Jon Corbett on programming language theory and announced the official poster artist for IPFS Connect Istanbul. <a href="https://fission.codes/blog/fission-fridays-september-15th-2023/" rel="nofollow noopener" target="_blank">https://fission.codes/blog/fission-fridays-september-15th-2023/</a> <a href="https://plnetwork.xyz/tags/programminglanguagetheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#programminglanguagetheory</a>

Causal IslandsFor episode 3 of the Causal Islands Podcast, we are joined by special guests <a href="https://merveilles.town/@nasser" class="u-url mention" rel="nofollow noopener" target="_blank">@nasser</a> and Jon Corbett to discuss their work creating Arabic and Cree programming languages and what they learned in the process. <a href="https://fission.codes/blog/causal-islands-podcast-ep03-alternatives-to-modern-programming-languages/" rel="nofollow noopener" target="_blank">https://fission.codes/blog/causal-islands-podcast-ep03-alternatives-to-modern-programming-languages/</a> <a href="https://plnetwork.xyz/tags/programminglanguagetheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#programminglanguagetheory</a>

Yaroslav KhnyginWhat are the best (and ideally still in print) textbooks that cover parsing expression grammars (PEGs) and Packrat parsers?<a href="https://mastodon.ie/tags/ComputerScience" class="mention hashtag" rel="nofollow noopener" target="_blank">#ComputerScience</a> <a href="https://mastodon.ie/tags/ProgrammingLanguages" class="mention hashtag" rel="nofollow noopener" target="_blank">#ProgrammingLanguages</a> <a href="https://mastodon.ie/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#ProgrammingLanguageTheory</a> <a href="https://mastodon.ie/tags/Programming" class="mention hashtag" rel="nofollow noopener" target="_blank">#Programming</a> <a href="https://mastodon.ie/tags/Parsers" class="mention hashtag" rel="nofollow noopener" target="_blank">#Parsers</a> <a href="https://mastodon.ie/tags/Parsing" class="mention hashtag" rel="nofollow noopener" target="_blank">#Parsing</a> <a href="https://mastodon.ie/tags/PEG" class="mention hashtag" rel="nofollow noopener" target="_blank">#PEG</a> <a href="https://mastodon.ie/tags/Learning" class="mention hashtag" rel="nofollow noopener" target="_blank">#Learning</a> <a href="https://mastodon.ie/tags/Textbooks" class="mention hashtag" rel="nofollow noopener" target="_blank">#Textbooks</a>

Yaroslav KhnyginWere there ever any attempts to somehow add multimethods (multiple dispatch) to Smalltalk? 🤔<a href="https://mastodon.ie/tags/Smalltalk" class="mention hashtag" rel="nofollow noopener" target="_blank">#Smalltalk</a> <a href="https://mastodon.ie/tags/ProgrammingLanguages" class="mention hashtag" rel="nofollow noopener" target="_blank">#ProgrammingLanguages</a> <a href="https://mastodon.ie/tags/OOP" class="mention hashtag" rel="nofollow noopener" target="_blank">#OOP</a> <a href="https://mastodon.ie/tags/ObjectOrientedProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#ObjectOrientedProgramming</a> <a href="https://mastodon.ie/tags/PLT" class="mention hashtag" rel="nofollow noopener" target="_blank">#PLT</a> <a href="https://mastodon.ie/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#ProgrammingLanguageTheory</a> <a href="https://mastodon.ie/tags/Programming" class="mention hashtag" rel="nofollow noopener" target="_blank">#Programming</a>

Recent searches

Search options

Administered by:

Server stats:

#programminglanguagetheory