Programming Languages

Languages

J: A high-performance language for data processing and parallel computing. J implementation in Nim
Z: A dialect for C that's immutable by default, resolves undefined behavior and uses an SMT solver to guarantee reference stability
Chapel: A parallel programming language that claims to have some novel ideas.
Catala: A DSL for representing laws by construction, designed to enable lawyers to certify laws. Interested in formal verification of legal documents, potentially.
Raku: A descendent of Perl, it features lots of additional features including fun grammar specifications.
Ante: 'The compile-time language'. Made by a Northeastern undergraduate.
Oak: Designed as a simple replacement for C.
Topshell: A functional, reactive scripting language.
Chef: An esoteric programming language designed to simultaneously represent recipes and programs.
Fennel: Lisp for Lua.
Whitespace: A programming language designed with only whitespace characters, ignoring all others. Any program that disregards whitespace can express a whitespace program within it. Fun to represent in laugnages that aren't indent-aware - these programs can also encode Whitespace within them!
Lux: A statically typed Lisp-like language for the JVM.
While: A language used in textbooks such as 'Principles of Program Analysis'.
PolyRPC: A 'multi-tier' functional programming language.
Steno: livecoding metalanguage
Unlambda: A minimal functional programming language based on combinatory logic meant to be a demonstration of pure functional programming
Vodka: A creative coding environment and language for structured editing for writers.
Play: A statically typed Forth!
Imba: A programming language for the web that finally handles full stack in all of the right waysLove the syntax!!! Great lessons from someone who knows how to teach as well - very easy to understand and get started with the language!

DSLs

MLang: A DSL created to represent and calculate the French tax code.
Dhall: langauge for system configuration
puzzlescript: language for puzzles!
Frink: The Frink is Good, the Unit is Evil
Alda: Make music!

Ahnfelt/funk: PROTOTYPE: A minimal scripting language - OOP via lambda func Programming Languages as Objects in Nature https://www.colm.net/open-source/ragel/ state machine compiler https://www.openpolicyagent.org/docs/latest/policy-language/ policy lang http://inform7.com/ dsl for text based adventures http://ebblang.org/ dsl for physical simulations http://terralang.org/ systems prog lang embedded in Lua http://optlang.org/ embedded lang for nonlinear least squares optimization https://hackage.haskell.org/package/accelerate embedded lang for array processing

also see https://jrslepak.github.io/publications/ https://tracery.io/ :: simple graphics programming language

Unison

A distributed programming language and editing environment for the modern web. A major inspiration for the projectional Text Editors project.

https://faust.grame.fr/ https://en.m.wikipedia.org/wiki/Datalog http://pepijndevos.nl/2018/10/03/behavior-trees-are-concatenative-programs.html behavior trees http://coconut-lang.org/ https://www.dangermouse.net/esoteric/piet.html https://effekt-lang.org/ effekt polymorphism

Work

https://hmc-cs111-fall2016.github.io/ class on DSLs https://github.com/google/evcxr https://github.com/hengestone/lua-languages programming languages targeting lua https://github.com/jeanqasaur/dsl-syllabus-fall-2016 class on dsls

Research

https://github.com/jdublu10/icfp2020-papers ICFP 2020 conf https://github.com/melling/ComputerLanguages someone's notes on computer languages

Lean

This'll be factored out when I learn more about Lean. https://github.com/uwdb/Cosette automated sql solver https://github.com/ImperialCollegeLondon/group-theory-game group theory in lean

blurring the curry howard line

https://www.youtube.com/watch?v=jrVPB-Ad5Gc&t=1870s&app=desktop 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

blurring the curry howard line

https://www.youtube.com/watch?v=jrVPB-Ad5Gc&t=1870s&app=desktop works on autonomous vehicles, fun stuff

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.

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!

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

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

???

https://www.reddit.com/r/gorillaz/comments/g980ui/rock_the_house_animation_by_%E3%83%96%E3%83%AB%E3%83%BC%E3%83%8F%E3%83%A0%E3%83%8F%E3%83%A0/ -- how do i do animations like this?

https://www.linkedin.com/mwlite/in/christopher-choquette-choo who is this dude? https://copetti.org/projects/ -- does writing on console architecture https://pydanny.blogspot.com/2011/08/github-is-my-resume.html?m=1 -- making a resume for github http://mjb.io/ -- wild!

Programming Languages

useful resources: https://github.com/wilbowma/pl-thesaurus -- too advanced for me

Adjunction

Whnen categories are Posets, adjunction is a Galois connection

Strong Monad

Monad

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

Reflection

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

https://www21.in.tum.de/~nipkow/TRaAT/ -- book benjamin had, it's a description of term rewriting problems, universal algebra, unification theory https://en.wikipedia.org/wiki/Rewriting

pl random link spit

fun languages

https://github.com/adam-mcdaniel/oakc fun alternative to c langauge https://github.com/psg-mit/smooth http://bloom-lang.net/ https://www.reddit.com/r/ProgrammingLanguages/comments/g2hhq0/statically_typed_language_with_a_flexible_macro/

https://www.reddit.com/r/ProgrammingLanguages/comments/avvma5/atto_an_insanely_tiny_selfhosted_functional/ https://www.reddit.com/r/haskell/comments/fz7heq/accidentally_exponential_in_a_compiler/ https://blog.josephmorag.com/posts/mcc2/ https://dl.acm.org/doi/abs/10.1145/301618.301637 https://github.com/mcoblenz/Obsidian https://adamant-lang.org/ http://www.mlton.org/ http://matt.might.net/articles/best-programming-languages/ https://chrisseaton.com/truffleruby/ https://futhark-lang.org/blog/2020-04-13-statically-linking-the-futhark-compiler.html https://www.reddit.com/r/ProgrammingLanguages/comments/awr3th/i_made_a_programming_language_based_on_cobol/ https://github.com/seanbaxter/circle http://blog.hydromatic.net/2020/02/25/morel-a-functional-language-for-data.html https://www.reddit.com/r/ProgrammingLanguages/comments/ecc1fo/design_flaws_in_futhark/ https://github.com/Storyyeller/IntercalScript https://vanemden.wordpress.com/2014/06/18/how-recursion-got-into-programming-a-comedy-of-errors-3/

haxe!

https://www.reddit.com/r/programming/comments/do220a/haxe_4_has_been_released/ cross platform language toolkit! https://www.reddit.com/r/ProgrammingLanguages/comments/eh1sfy/carpentry_compiler/ https://blog.darknedgy.net/technology/2020/05/02/0/

verification

https://www.cs.princeton.edu/~appel/certicoq/ https://vst.cs.princeton.edu/ building verified software

parsing

https://www.reddit.com/r/ProgrammingLanguages/comments/dszj7b/parse_dont_validate/ https://nothings.org/computer/lexing.html -- lexing https://softwareengineering.stackexchange.com/questions/338665/when-to-use-a-parser-combinator-when-to-use-a-parser-generator https://www.reddit.com/r/perl6/comments/73tjdo/an_outline_of_federico_tomassettis_a_guide_to/ 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

https://www.typescriptlang.org/docs/handbook/advanced-types.html#index-types-and-index-signatures http://reasonableapproximation.net/2019/05/05/hindley-milner.html http://prl.ccs.neu.edu/gtp https://ncatlab.org/nlab/show/pure+type+system https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/ great writeup about pa paper

redex

https://www.youtube.com/watch?v=BuCRToctmw0 -- run your research - talk on redex https://redex.racket-lang.org/ a dsl for specifying and debugging operational semantics

compilers

compiler neat thing improving compiler correctness using formal methods http://www.keystone-engine.org/ https://jamespackard.me/ https://ollef.github.io/blog/posts/speeding-up-sixty.html https://whalesalad.com/blog/doing-python-configuration-right https://en.m.wikipedia.org/wiki/Multi-pass_compiler https://en.m.wikipedia.org/wiki/Data-flow_analysis https://www.reddit.com/r/ProgrammingLanguages/comments/a60i0m/unlike_ordinary_jit_compilers_for_other_languages/

https://gist.github.com/cellularmitosis/1f55f9679f064bcff02905acb44ca510#simple-compiler-codebases-to-study crazy compilers good stuff

https://zserge.com/posts/jvm/ 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! https://www.cs.cmu.edu/~janh/courses/411/16/ compiler design course at cmu. supposedly good material

https://stackoverflow.com/questions/6264249/how-does-the-compilation-linking-process-work#6264256 https://www.cprogramming.com/compilingandlinking.html

https://www.youtube.com/watch?v=Os7FE3J-U5Q&app=desktop writing a nanopass compiler https://en.m.wikipedia.org/wiki/Intermediate_representation good reading https://en.m.wikipedia.org/wiki/Three-address_code https://en.m.wikipedia.org/wiki/Static_single_assignment_form https://catalog.princeton.edu/catalog/SCSB-8534958 -- benjamin's favorite compilers book http://www.ocamlpro.com/2020/03/23/ocaml-new-best-fit-garbage-collector/ http://www.aosabook.org/en/llvm.html -- on llvm https://en.wikipedia.org/wiki/Alan_Perlis -- pl research, won turing award or something type preserving compilation for large scale optimizing object oriented compilers how efficient can objects be? https://v8.dev/blog/pointer-compression -- pointer compression in v8 https://en.wikipedia.org/wiki/Optimizing_compiler https://dl.acm.org/doi/10.1145/1375581.1375604 https://gcc.gnu.org/onlinedocs/gcc/Optimize-Options.html https://www.cs.cornell.edu/courses/cs4410/2014fa/ https://www.reddit.com/r/ProgrammingLanguages/comments/fqt0fo/the_strange_case_of_dr_function_and_mr_type/fm0vurc/?context=1 http://prl.ccs.neu.edu/blog/2020/01/15/the-typed-racket-optimizer-vs-transient/ https://docs.racket-lang.org/ts-guide/index.html https://www.reddit.com/r/ProgrammingLanguages/comments/f3ekao/i_built_a_2d_gridbased_esoteric_language_with_a/ https://esolangs.org/wiki/2014 esolang only working in 2014 https://esolangs.org/wiki/Efghij esolang that interacts with the physical world via a jenga-based game, manually interpreted and executed by the programmer according to the specification https://esolangs.org/wiki/Ziim 2d language reliant entirely on unicode arrows https://matklad.github.io/2020/04/15/from-pratt-to-dijkstra.html https://www.reddit.com/r/ProgrammingLanguages/comments/e1vv55/c3_a_clike_language_now_has_a_domain/ https://www.reddit.com/r/ProgrammingLanguages/comments/a0yyfc/plam_for_anyone_exploring_%CE%BBcalculus/

https://www.reddit.com/r/ProgrammingLanguages/comments/g1wd0v/but_what_if_we_put_modifiers_after_the_keyword/

https://blog.sigplan.org/2020/07/29/increasing-the-impact-of-pl-research/ a meta article on impactful pl research http://craftinginterpreters.com/ https://github.com/glaretechnologies/winter

https://www.zinkov.com/posts/2019-02-17-why-program-synthesis/ program synthesis why? https://loglo.app/ turn yaml into cnc https://tixy.land/ fun language for creative code golfing

run your research paper is probably cool! https://m.youtube.com/watch?v=jdn617M3-P4 hitchhiker trees: cool functional data structure https://wiki.xxiivv.com/site/fractran.html

https://ziglearn.org/ learn zig

Hobby kernel written in Zig https://malleable.systems/catalog/

On the expressive power of programming languages - ScienceDirect https://github.com/iitalics/Opal

single file implementations of various programming languages https://www.ponylang.io/

Contextual types meet mechanized metatheory! https://github.com/lasp-lang/lasp https://github.com/NicklasBoto/BruSKI debrujin to ski unlambda compiler https://github.com/Storyyeller/IntercalScript intercalscript programming language https://github.com/taichi-dev/taichi differentiable programming languages https://github.com/jasonhemann/microKanren https://github.com/mame/quine-relay https://github.com/lasp-lang/partisan distributed computing with Elixir

halide: language for fast and portable data parallel computation factor programming language: concatenative programming thats stack based https://github.com/Gwion/Gwion: strongly typedMusic programming language https://github.com/unisonweb/unison a friendly web programming language

https://github.com/thesephist/schrift 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

forth in the early years
- evolved throughout the 60s, only a single programmer!
- "unique combination of ingredients"
- context free text based language combining words that have a variety of (arguably) advanced features, and runnable on small embedded systems with sufficient

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

https://github.com/meilisearch/MeiliSearch typo tolerant search engine https://github.com/Shen-Language/shen-sources shen programming language https://news.ycombinator.com/item?id=23252448 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 https://www.reddit.com/r/cscareerquestions/comments/9ujawa/programming_language_theory_jobs/ 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&#39;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 https://www.classes.cs.uchicago.edu/archive/2020/spring/32001-1/ the death of prolog https://en.m.wikipedia.org/wiki/Simula 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

https://www.reddit.com/r/ProgrammingLanguages/comments/fxc504/do_you_know_any_interesting_talks_about_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 languages Employment