u/mttdin r/ProgrammingLanguages • Recommends
Basic Mechanics of Operational Semantics
0:00 / 0:00
#operationalsemantics#typesystems#abstractmachines
Basic Mechanics of Operational Semantics
ACM SIGPLAN
11K subscribers • 61 videos on Hallway
- Recommended by 1 person: 1 in engineering communities.
- Presented by David Van Horn
Intermediate. Assumes working knowledge.
6.3K views5 years ago1 recommendation
Computer scienceProgramming languagesComputation and complexityFormal methods and verification
David Van Horn provides a crash course on reading and understanding operational semantics in programming language research.
David Van Horn icfp20.sigplan.org/details/PLMW-icfp-2020/5/Basic-Mechanics-… In this talk, I’ll give a crash course in reading and understanding the dense notational conventions often employed in programming language research papers and try to motivate why these conventions are used in the first place. We’ll cover different forms of operational semantics such as big-step and small-step semantics, the relation between SOS-style and evaluation-style presentations, and notions such as environments, substitution, abstract machines, and type systems. This talk will by no means provide complete coverage of these topics, but should give you just enough to get a sense of what is going on in any given ICFP paper you happen to pick up.Why it's here
1 person recommends thisu/DonaldPShimodain r/ProgrammingLanguages • Mentions
On “Understanding mathematical notation”
I *love* TAPL. Great book.
I would also point you to the very recently given (~2 weeks ago) PLMW@SPLASH presentation Basic Mechanics of Operational Semantics by Professor David Van Horn of the University of Maryland. The presentation is about 30 minutes and was geared towards an audience of the advanced undergraduate or new graduate student in programming languages. (PLMW is the Programming Languages Mentoring Workshop, hosted a few times a year, where established PL researchers give presentations of advice and basic PL topics to new researchers in the field.)
Operational semantics is a way of writing semantic rules that I find more intuitive than denotational semantics (which is what we…
u/Irony238in r/ProgrammingLanguages • Mentions
On “Understanding mathematical notation”
I can recommend this talk from PLMW (Programming languages Mentoring Workshop) at ICFP this year. It introduces some of the common notations in PL papers (including inference rules) in a beginner friendly way. I don't think it covers Type Systems though.
EDIT: I was made aware that I accidentally linked to the whole playlist. This is the talk I wanted to link to.
u/DonaldPShimodain r/ProgrammingLanguages • Mentions
On “Experiences with structured format to describe language concepts and rules?”
Yes, Redex is probably what OP is looking for. It's a language implemented in Racket that can take a syntax and an operational semantics and produces an interpreter for the language described by them. You can also use it to check that your semantics does what you think it does.
There's a textbook: "Semantics Engineering with PLT Redex", written by Robby (the professor mentioned) as well as Matthias Felleisen (Northeastern University, originator of the Racket project) and Matthew Flatt (University of Utah, an original member of the Racket project like Robby). It's expensive and a bit outdated, but it's cool because it's written in two parts: one about only semantics, and the other about the…
u/DonaldPShimodain r/ProgrammingLanguages • Mentions
On “Absolutely introductory books / courses to PL theory?”
At PLMW@ICFP 2020 (that's the Programming Languages Mentoring Workshop at the International Conference on Functional Programming, 2020), David Van Horn gave a talk titled "The Basic Mechanics of Operational Semantics". The purpose was to introduce newcomers to PL research to this syntax (and some more) so they could begin to read papers and the like.
- YouTube video of the talk
- slides from the talk