*Last Call*

I have a #PhD position for UK students, available with myself and @bentnib

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 2025

You will belong to @StrathCyber and @mspstrath, as well as gaining access to @spli

https://www.strath.ac.uk/studywithus/postgraduateresearchphdopportunities/science/computerinformationsciences/towardstype-drivenassuranceofcommunicatingsystems/

(Ignore the deadline on the advert)

Please spread the words.

#dependentTypes #formalMethods #idris #programmingLanguageTheory #typeTheory #idris2 #computerSecurity #cybersecurity #securityByDesign #secureByDesign

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

I have a funded #PhD position for UK students, available with myself and @bentnib

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 2025

You will belong to @StrathCyber and @mspstrath, as well as gaining access to @spli

For now more details about the project are on my personal website.

https://tyde.systems/page/position/2025-jarss/

Please spread the words.

#dependentTypes #formalMethods #idris #programmingLanguageTheory #typeTheory #idris2 #computerSecurity #cybersecurity #securityByDesign #secureByDesign

Just got paid to write a formal grammar.

Does this make me a professional language writer?

#Programming #ProgrammingLanguageTheory

Type checking approach to estimating sensitivity bounds in differential privacy: Gradual Differentially Private Programming - https://cacm.acm.org/latin-america-regional-special-section/gradual-differentially-private-programming/

#DifferentialPrivacy #ProgrammingLanguageTheory

@thephd @ehashman Ok but tbf #goLang ignored the previous 50 years of #programmingLanguageTheory, confirming that Rob Pike and Ken Thompson cannot design a #programmingLanguage to save their life, instead making a worse #javeLang

Even #Rust can do a map a Vec and return another Vec in a one-liner

Next Wednesday I will be visiting St Andrews for the first Scottish Programming Languages Seminar of 2024. The program looks pretty interesting:
https://scottish-pl-institute.github.io/spls/meetings/2024/march/
#ProgrammingLanguageTheory #PLT

An interesting resource for learning #TypeTheory and adjacent areas like #CategoryTheory:

“learn-tt”, Daniel Gratzer (https://github.com/jozefg/learn-tt).

#Types #PLT #ProgrammingLanguageTheory #PLDI

@jnkrtech

#FunctionalProgramming #TypeTheory #Scala #ProgrammingLanguageTheory #plt 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)

A 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?

#FunctionalProgramming #TypeTheory #Scala #ProgrammingLanguageTheory #plt

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

This week, we hosted a fascinating discussion with @nasser and Jon Corbett on programming language theory and announced the official poster artist for IPFS Connect Istanbul. https://fission.codes/blog/fission-fridays-september-15th-2023/ #programminglanguagetheory

For episode 3 of the Causal Islands Podcast, we are joined by special guests @nasser and Jon Corbett to discuss their work creating Arabic and Cree programming languages and what they learned in the process. https://fission.codes/blog/causal-islands-podcast-ep03-alternatives-to-modern-programming-languages/ #programminglanguagetheory

What are the best (and ideally still in print) textbooks that cover parsing expression grammars (PEGs) and Packrat parsers?

#ComputerScience #ProgrammingLanguages #ProgrammingLanguageTheory #Programming #Parsers #Parsing #PEG #Learning #Textbooks

Were there ever any attempts to somehow add multimethods (multiple dispatch) to Smalltalk? 🤔

#Smalltalk #ProgrammingLanguages #OOP #ObjectOrientedProgramming #PLT #ProgrammingLanguageTheory