Ahnfelt/funk: PROTOTYPE: A minimal scripting language - OOP via lambda func Programming Languages as Objects in Nature state machine compiler policy lang dsl for text based adventures dsl for physical simulations systems prog lang embedded in Lua embedded lang for nonlinear least squares optimization embedded lang for array processing behavior trees effekt polymorphism

Work class on DSLs programming languages targeting lua class on dsls

Research ICFP 2020 conf someone's notes on computer languages


This'll be factored out when I learn more about Lean. automated sql solver group theory in lean

blurring the curry howard line works on autonomous vehicles, fun stuff

typically using languages iwth proof assistants. however, actuation systems in carshave real time constraints, so lazy evaluation or nondeterministic memory management is not valid. this is typically done in c or cpp. pulling a c program from a coq proof ?

programs :: foramlized syntactically, but modeled semantically. denotational semantics map number to some set :: ie some u8 integer fits within one set. map syntactic objects to universal mathematics with such denotational semantics

typing rules: tau - a : A, f:A -> B

tau |- a

cannot capture everything with type theory? dependent types end up capturing everything. can provide complete specification of a program's behavior in the dependent type theory.

curry-howard correspondance :: a correspondence between program and proof! we know we can reason about our programs from a dependent type theory, but what is this gap called? specifying program in the types: can make assertions about the correctness of this code.

why dependent types matter paper. rust provides subset for representing dependent typed behavior in our programs. type level definition of the natural numbers, for example!

these programs can be fully represented in state machines! the entire system and communication protocols can be captured with such a state machine, and this state machine can be represented in a rust type system

state :: sum type. type family adjacency; types that are members of the type family are adjacent to each of these states.

can use demotational semantics to convert rust semantics to agda :: and as agda has full dependent types. using agda allows us to mechanize semantic function ! agda has a notion of proofs and may soon have a notion of tactics. proving things foundationally in agda could be doable once we have the specification of the program in its own domain

state machines :: behold the program counter as everything is tracked at compile time. not easy in this representation to track a state machine in terms of program handlers.

church numerals :: general way of using a function to produce numbers program that extracts information from a rust program and stick the semantics in agda

future reading

toy lang

powerful programming language type level programming aliasing and ownership the art of code prog synth at pldi

??? -- how do i do animations like this? who is this dude? -- does writing on console architecture -- making a resume for github -- wild!

Programming Languages

useful resources: -- too advanced for me


Whnen categories are Posets, adjunction is a Galois connection

Strong Monad


Kleisli trible, s4 possibility mdality when category is defined as poset, monad is a closure operator


when categories are posets, this is a galois surjection

Right Adjoint

In order theory, right adjoint of Galois connection is upper adjoint in abstract interpretation, this is Concretization function

Left Adjoint

in order theory: left adjoint of galois connection is lower adjoint in abstract interpretation, this is abstract function

Galois Connection

term rewriting -- book benjamin had, it's a description of term rewriting problems, universal algebra, unification theory

pl random link spit -- overview of great works in pl to know before diving in! -- software foundations -- foundations in agda! for free! -- excellent essay on the importance of naming -- intro to probabilistic prgrammign ! -- writing a quick lisp interpreter in haskell -- building modern functional compiler from first principles parsing --basically indenting and dedenting with lexer just like any other parens -- context-free parsing of strings algorithm -- introduction to writing proofs about computer programs -- haskell-inspired purely functional programming language with dependent types -- derivatives of language constructs - whoah! -- proofs that require no trusted setup designing a simple racket dsl -- hack your own language / building extensible systems : learn more about it! please! -- the book on crafting interpreters!msg/racket-users/vN_1uUJZnXo/5bXiMEBvCgAJ -- arguments aboutsurface syntax of racket -- racket on chez scheme for performance optimizations! synthesizing programs from input and output!! wow!! program synthesis looks like such a cool thing

fun languages fun alternative to c langauge

haxe! cross platform language toolkit! bytecode interpreter comments

verification building verified software

parsing -- lexing shunting yard algorithm : used to parse expressions in infix notation ! in parser generator: .mly file uses infix things with Shunting Yard Algorithm under the hood !!

type systems great writeup about pa paper

redex -- run your research - talk on redex a dsl for specifying and debugging operational semantics


compiler neat thing improving compiler correctness using formal methods crazy compilers good stuff how to write a toy jvm -- try this and put it on github! fun small thing to mess around with. add more to it, add new things, mess aroundand have fun! compiler design course at cmu. supposedly good material writing a nanopass compiler good reading -- benjamin's favorite compilers book -- on llvm -- pl research, won turing award or something type preserving compilation for large scale optimizing object oriented compilers how efficient can objects be? -- pointer compression in v8 esolang only working in 2014 esolang that interacts with the physical world via a jenga-based game, manually interpreted and executed by the programmer according to the specification 2d language reliant entirely on unicode arrows a meta article on impactful pl research program synthesis why? turn yaml into cnc fun language for creative code golfing

run your research paper is probably cool! hitchhiker trees: cool functional data structure learn zig

Hobby kernel written in Zig

On the expressive power of programming languages - ScienceDirect

single file implementations of various programming languages

Contextual types meet mechanized metatheory! debrujin to ski unlambda compiler intercalscript programming language differentiable programming languages distributed computing with Elixir

halide language for fast and portable data parallel computation factor programming language concatenative programming thats stack based strongly typedMusic programming language a friendly web programming language an experimental runtime for ink lang alpaca: ml style functional programming for the erlang vm self hosted forth implementation

bytecode interpreter in x86 asm multitasking Z81 forth pl thesaurus

atto: super simple self hosted programming language BASIC interpreter in Go Eve a 'human first' programming language SAIL architecture definition language (inCoq for describing ISAs of processors incremental parsing system for programming tools typo tolerant search engine shen programming language alloy - os lang and analyzer for software modeling

type level programming What is the Forth programming language? Total functional programming - Wikipedia

adam-mcdaniel/oakc: A portable programming language with an incredibly comp psg-mit/smooth: An arbitrary-precision differentiable programming language. on influential dead languages masaeedu/ulc: Untyped lambda calculus Let’s Build A Simple Interpreter. Part 1. William E Byrd - Relational Interpreters, Program Synthesis, and Barliman - Let’s Build A Simple Interpreter. Part 1. - Ruslan's Blog Which languages have weak references? - ProgrammingLanguages The Frink is Good, the Unit is Evil • Hillel Wayne A few questions about parser design - ProgrammingLanguages

Chapel: Productive Parallel Programming Jsoftware

DM's Esoteric Programming Languages - Piet

sarah jeong on Twitter: "If they think declaring code is creative enough to merit copyright protection, aren't we left with the conclusion that *languages* are protectable?" / Twitter gluon-lang/gluon: A static, type inferred and embeddable language written i

Seven Languages in Seven Weeks: A Pragmatic Guide to Learning Programming L

Underappreciated programming language concepts or features? : ProgrammingLa

Raku Programming Language the death of prolog Parsing with derivatives | Proceedings of the 16th ACM SIGPLAN international conference on Functional programming Robby Findler: Concolic Testing with Higher-Order Inputs - YouTube [1911.04523] A Simple Differentiable Programming Language The SLam calculus | Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages Val on Programming: What makes a good REPL? on writing a pl

writing a toy jvm The Zephyr Abstract Syntax Description Language What is Zephyr ASDL? ICFP Contest 2019 Pharo - Welcome to Pharo! The expression problem

how to get a job in programming languagesEmployment

Programming Languages as Objects in Nature Daniel P. Friedman: A Celebration

jfecher/bidirectional jfecher/ante

simplelang ai dungeon dragon program interdisciplinary applications of artificial intelligence a fun minimal scripting language programming with a differentiable forth interpreter

Effekt: A language with effect handlers and a lightweight effect system - P


increasing the impact of pl research, connecting it to reality! Hardware dsls dependent type systems aas macros paper : ) cool phd student of will bowman! work on the Vale language whirlwind tour of lagnauges with some opinions Racket cool ideas, reducing the cost of structured data, etc. Factor vs. Forth (from a Forth programmer) | Hacker News Joy (programming language) - Wikipedia Self (programming language) - Wikipedia simple and clever programming language Hazel A live functional programming environment history of dead languages pl programming with syntax highlighting parsing strategies test case generation !! tons of great reading material. :: an extension of scheme that not only allows for metaprogramming, but also meta-modification of the interpreter it's running on! any program can modify the behavior of the interpreter. nuts!


interview about unlambda

typetheorypodcast.comprobably a good podcast