Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mathstodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance for maths people. We have LaTeX rendering in the web interface!

Administered by:

Server stats:

3K
active users

mathstodon.xyz: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

#programminglanguagetheory

0 posts0 participants0 posts today
jnkrtech<p>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.</p><p>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?</p><p><a href="https://social.treehouse.systems/tags/lean" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>lean</span></a> <a href="https://social.treehouse.systems/tags/programminglanguagetheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>programminglanguagetheory</span></a> <a href="https://social.treehouse.systems/tags/PLT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>PLT</span></a> <a href="https://social.treehouse.systems/tags/proofs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>proofs</span></a> <a href="https://social.treehouse.systems/tags/TAPL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TAPL</span></a> <a href="https://social.treehouse.systems/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Lean4</span></a></p>
Jan de Muijnck-Hughes<p>I have a funded <a href="https://discuss.systems/tags/PhD" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>PhD</span></a> position for UK students, available with myself and <span class="h-card" translate="no"><a href="https://types.pl/@bentnib" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>bentnib</span></a></span> </p><p>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.</p><p>Deadline: Thursday 20th March 2025</p><p>You will belong to <span class="h-card" translate="no"><a href="https://mastodon.acm.org/@StrathCyber" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>StrathCyber</span></a></span> and <span class="h-card" translate="no"><a href="https://mastodon.acm.org/@mspstrath" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>mspstrath</span></a></span>, as well as gaining access to <span class="h-card" translate="no"><a href="https://mastodon.scot/@spli" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>spli</span></a></span> </p><p>For now more details about the project are on my personal website.</p><p><a href="https://tyde.systems/page/position/2025-jarss/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">tyde.systems/page/position/202</span><span class="invisible">5-jarss/</span></a></p><p>Please spread the words. </p><p><a href="https://discuss.systems/tags/dependentTypes" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>dependentTypes</span></a> <a href="https://discuss.systems/tags/formalMethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalMethods</span></a> <a href="https://discuss.systems/tags/idris" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>idris</span></a> <a href="https://discuss.systems/tags/programmingLanguageTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>programmingLanguageTheory</span></a> <a href="https://discuss.systems/tags/typeTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>typeTheory</span></a> <a href="https://discuss.systems/tags/idris2" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>idris2</span></a> <a href="https://discuss.systems/tags/computerSecurity" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>computerSecurity</span></a> <a href="https://discuss.systems/tags/cybersecurity" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>cybersecurity</span></a> <a href="https://discuss.systems/tags/securityByDesign" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>securityByDesign</span></a> <a href="https://discuss.systems/tags/secureByDesign" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>secureByDesign</span></a></p>
b4ux1t3 :trek_ds9_sisko:#1️⃣<p>Just got paid to write a formal grammar.</p><p>Does this make me a professional language writer?</p><p><a href="https://hachyderm.io/tags/Programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Programming</span></a> <a href="https://hachyderm.io/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProgrammingLanguageTheory</span></a></p>
Maciek<p>Type 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 noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">cacm.acm.org/latin-america-reg</span><span class="invisible">ional-special-section/gradual-differentially-private-programming/</span></a></p><p><a href="https://hachyderm.io/tags/DifferentialPrivacy" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DifferentialPrivacy</span></a> <a href="https://hachyderm.io/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProgrammingLanguageTheory</span></a></p>
DocRekd<p><span class="h-card" translate="no"><a href="https://pony.social/@thephd" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>thephd</span></a></span> <span class="h-card" translate="no"><a href="https://cloudisland.nz/@ehashman" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>ehashman</span></a></span> Ok but tbf <a href="https://hachyderm.io/tags/goLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>goLang</span></a> ignored the previous 50 years of <a href="https://hachyderm.io/tags/programmingLanguageTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>programmingLanguageTheory</span></a>, confirming that Rob Pike and Ken Thompson cannot design a <a href="https://hachyderm.io/tags/programmingLanguage" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>programmingLanguage</span></a> to save their life, instead making a worse <a href="https://hachyderm.io/tags/javeLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>javeLang</span></a></p><p>Even <a href="https://hachyderm.io/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rust</span></a> can do a map a Vec and return another Vec in a one-liner</p>
pera<p>Next Wednesday I will be visiting St Andrews for the first Scottish Programming Languages Seminar of 2024. The program looks pretty interesting:<br><a href="https://scottish-pl-institute.github.io/spls/meetings/2024/march/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">scottish-pl-institute.github.i</span><span class="invisible">o/spls/meetings/2024/march/</span></a><br><a href="https://mastodon.social/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProgrammingLanguageTheory</span></a> <a href="https://mastodon.social/tags/PLT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>PLT</span></a></p>
रञ्जित (Ranjit Mathew)<p>An interesting resource for learning <a href="https://mastodon.social/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TypeTheory</span></a> and adjacent areas like <a href="https://mastodon.social/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CategoryTheory</span></a>:</p><p>“learn-tt”, Daniel Gratzer (<a href="https://github.com/jozefg/learn-tt" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">github.com/jozefg/learn-tt</span><span class="invisible"></span></a>).</p><p><a href="https://mastodon.social/tags/Types" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Types</span></a> <a href="https://mastodon.social/tags/PLT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>PLT</span></a> <a href="https://mastodon.social/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProgrammingLanguageTheory</span></a> <a href="https://mastodon.social/tags/PLDI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>PLDI</span></a></p>
fanf42<p><span class="h-card" translate="no"><a href="https://social.treehouse.systems/@jnkrtech" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>jnkrtech</span></a></span> </p><p><a href="https://social.treehouse.systems/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://social.treehouse.systems/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TypeTheory</span></a> <a href="https://social.treehouse.systems/tags/Scala" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Scala</span></a> <a href="https://social.treehouse.systems/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProgrammingLanguageTheory</span></a> <a href="https://social.treehouse.systems/tags/plt" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>plt</span></a> o thing it is but iirc there was subtleties.<br>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).<br>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)</p>
jnkrtech<p>A few questions that have been nagging me:</p><p>- Is Scala’s theory of dependent objects a generalization of system f sub omega?<br>- If so, is Scala the only mainstream language that implements f sub omega?<br>- 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?</p><p><a href="https://social.treehouse.systems/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://social.treehouse.systems/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TypeTheory</span></a> <a href="https://social.treehouse.systems/tags/Scala" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Scala</span></a> <a href="https://social.treehouse.systems/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProgrammingLanguageTheory</span></a> <a href="https://social.treehouse.systems/tags/plt" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>plt</span></a></p>
jnkrtech<p>Is there current research on formally verifying “open world” extensible object-oriented code?</p><p>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 noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">drops.dagstuhl.de/opus/volltex</span><span class="invisible">te/2017/7274/pdf/LIPIcs-ECOOP-2017-29.pdf</span></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.</p><p><a href="https://social.treehouse.systems/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://social.treehouse.systems/tags/PLT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>PLT</span></a> <a href="https://social.treehouse.systems/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProgrammingLanguageTheory</span></a> <a href="https://social.treehouse.systems/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TypeTheory</span></a> <a href="https://social.treehouse.systems/tags/TAPL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TAPL</span></a> <a href="https://social.treehouse.systems/tags/TypesAndProgrammingLanguages" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TypesAndProgrammingLanguages</span></a> <a href="https://social.treehouse.systems/tags/ProofAssistants" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProofAssistants</span></a><br><a href="https://social.treehouse.systems/tags/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</span></a> <a href="https://social.treehouse.systems/tags/Isabelle" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Isabelle</span></a> <a href="https://social.treehouse.systems/tags/HOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HOL</span></a> <a href="https://social.treehouse.systems/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Lean4</span></a> <a href="https://social.treehouse.systems/tags/Idris" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Idris</span></a> <a href="https://social.treehouse.systems/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a></p>
Fission<p>This week, we hosted a fascinating discussion with <span class="h-card"><a href="https://merveilles.town/@nasser" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>nasser</span></a></span> 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 noreferrer" target="_blank"><span class="invisible">https://</span><span class="ellipsis">fission.codes/blog/fission-fri</span><span class="invisible">days-september-15th-2023/</span></a> <a href="https://plnetwork.xyz/tags/programminglanguagetheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>programminglanguagetheory</span></a></p>
Causal Islands<p>For episode 3 of the Causal Islands Podcast, we are joined by special guests <span class="h-card"><a href="https://merveilles.town/@nasser" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>nasser</span></a></span> 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 noreferrer" target="_blank"><span class="invisible">https://</span><span class="ellipsis">fission.codes/blog/causal-isla</span><span class="invisible">nds-podcast-ep03-alternatives-to-modern-programming-languages/</span></a> <a href="https://plnetwork.xyz/tags/programminglanguagetheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>programminglanguagetheory</span></a></p>
Yaroslav Khnygin<p>What are the best (and ideally still in print) textbooks that cover parsing expression grammars (PEGs) and Packrat parsers?</p><p><a href="https://mastodon.ie/tags/ComputerScience" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ComputerScience</span></a> <a href="https://mastodon.ie/tags/ProgrammingLanguages" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProgrammingLanguages</span></a> <a href="https://mastodon.ie/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProgrammingLanguageTheory</span></a> <a href="https://mastodon.ie/tags/Programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Programming</span></a> <a href="https://mastodon.ie/tags/Parsers" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Parsers</span></a> <a href="https://mastodon.ie/tags/Parsing" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Parsing</span></a> <a href="https://mastodon.ie/tags/PEG" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>PEG</span></a> <a href="https://mastodon.ie/tags/Learning" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Learning</span></a> <a href="https://mastodon.ie/tags/Textbooks" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Textbooks</span></a></p>
Yaroslav Khnygin<p>Were there ever any attempts to somehow add multimethods (multiple dispatch) to Smalltalk? 🤔</p><p><a href="https://mastodon.ie/tags/Smalltalk" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Smalltalk</span></a> <a href="https://mastodon.ie/tags/ProgrammingLanguages" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProgrammingLanguages</span></a> <a href="https://mastodon.ie/tags/OOP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>OOP</span></a> <a href="https://mastodon.ie/tags/ObjectOrientedProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ObjectOrientedProgramming</span></a> <a href="https://mastodon.ie/tags/PLT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>PLT</span></a> <a href="https://mastodon.ie/tags/ProgrammingLanguageTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProgrammingLanguageTheory</span></a> <a href="https://mastodon.ie/tags/Programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Programming</span></a></p>
SearchLive feeds
About