Relational Interpreters, Program Synthesis, and Barliman
summary
miniKanren encodes a Scheme relational interpreter so the system synthesizes code by running eval backwards; it actually generates quines, 99 distinct programs that evaluate to "I love you", and reconstructs append from input/output examples. A prototype IDE called Barliman ties it together. Performance work claims up to ~nine orders of magnitude speedup over the naive version. The approach yields concrete programs and surprising multiplicities of answers rather than abstract examples.
AI-written summary · about
chapters (19)
- 0:00Intro
- 0:19I love Scheme
- 2:10Mini Cameron
- 2:27Why use Mini Cameron
- 3:04My first program
- 4:02I knew how to program
- 5:48I want a programming language
- 6:31Lollipop driven development
- 6:48Inference rules
- 7:27Computer science metanotation
- 7:44Dougs Math Aquarium
- 8:00Mandelbrot
- 8:33Metanotation
- 8:54MiniCameron
- 12:02Loading a file
- 12:40Show of hands
- 15:29List processing
- 17:51Rules for interpreter
- 21:26Lollipop Land
related talks
40mYou are a Program Synthesizer
20mSemantic Reification: A New Paradigm for Random Program Generation
56mThe Rational Programmer, An Investigative Method for Programming Language Prag...
17mPushing the Limit of 1-Minimality of Language-Agnostic Program Reduction
28mLanguage Support for Property-Based Testing
30mGenerating Conforming Programs With Xsmith
30mConstrained generation of well-typed programs
20mDerivative-Guided Symbolic Execution