|
Change #56425
2020-03-06
13:07:40
|
create
Calagator::Event
1250476946
Public Tech Talk: “Adventures in Type-directed Programming”
Roll back
| description |
nil |
→ |
“My programs just write themselves!” This phrase is frequently exclaimed by users of functional programming languages with advanced type systems who observe that rich types often guide them directly towards correct programs. In reality, this paradigm known as type-directed programming is far from automatic. To take advantage of rich types, a developer must reason carefully and precisely about the types of their programs, a seemingly mechanical, yet cognitively demanding process.
To this end, I will describe our efforts to understand better and ultimately automate the type-directed programming process. Our primary technique is type-directed program synthesis, where we derive synthesis algorithms from type checking systems, allowing us to build synthesizers that take advantage of rich types. In addition to describing the type-directed program synthesis process, I will present Scythe, a program assistant for type-directed programming in the Haskell programming language, and our next steps towards evolving Scythe into a next-generation live programming assistant built upon program synthesis technology. |
| end_time |
nil |
→ |
2020-03-13 12:00:00 -0700 |
| id |
nil |
→ |
1250476946 |
| start_time |
nil |
→ |
2020-03-13 11:00:00 -0700 |
| title |
nil |
→ |
Public Tech Talk: “Adventures in Type-directed Programming” |
| url |
nil |
→ |
https://galois.com/blog/2020/03/public-tech-talk-adventures-in-type-directed-programming/ |
| venue_id |
nil |
→ |
202396496 |
|