Tagged "Programming Languages"

Implementing and Verifying "Static Program Analysis" in Agda, Part 1: Lattices
4965 words, about 24 minutes to read.
This is the first post in a series on static program analysis in Agda. See the introduction for a little bit more context. ...

Implementing and Verifying "Static Program Analysis" in Agda, Part 0: Intro
800 words, about 4 minutes to read.
Some years ago, when the Programming Languages research group at Oregon State University was discussing what to read, the Static Program Analysis lecture notes came up. ...

Bergamot: Exploring Programming Language Inference Rules
2421 words, about 12 minutes to read.
Inference Rules and the Study of Programming Languages In this post, I will talk about inference rules, particularly in the field of programming language theory. ...

A Verified Evaluator for the Untyped Concatenative Calculus
6826 words, about 33 minutes to read.
Earlier, I wrote an article in which I used Coq to encode the formal semantics of Dawn’s Untyped Concatenative Calculus , and to prove a few things about the minilanguage. ...

Formalizing Dawn in Coq
4373 words, about 21 minutes to read.
The Foundations of Dawn article came up on Lobsters recently. In this article, the author of Dawn defines a core calculus for the language, and provides its semantics. ...

A Typesafe Representation of an Imperative Language
4159 words, about 20 minutes to read.
A recent homework assignment for my university’s programming languages course was to encode the abstract syntax for a small imperative language into Haskell data types. ...

Meaningfully Typechecking a Language in Idris, With Tuples
2232 words, about 11 minutes to read.
Some time ago, I wrote a post titled Meaningfully Typechecking a Language in Idris. I then followed it up with Meaningfully Typechecking a Language in Idris, Revisited. ...

Meaningfully Typechecking a Language in Idris, Revisited
2970 words, about 14 minutes to read.
Some time ago, I wrote a post titled Meaningfully Typechecking a Language in Idris. The gist of the post was as follows: ...

Creating Recursive Functions in a Stack Based Language
1996 words, about 10 minutes to read.
In CS 381, Programming Language Fundamentals, many students chose to implement a stack based language. Such languages are very neat, but two of the requirements for such languages may, at first, seem somewhat hard to satisfy: ...

Meaningfully Typechecking a Language in Idris
2419 words, about 12 minutes to read.
This term, I’m a TA for Oregon State University’s Programming Languages course. The students in the course are tasked with using Haskell to implement a programming language of their own design. ...

A Language for an Assignment  Homework 3
4155 words, about 20 minutes to read.
It rained in Sunriver on New Year’s Eve, and it continued to rain for the next couple of days. So, instead of going skiing as planned, to the dismay of my family and friends, I spent the majority of those days working on the third language for homework 3. ...

A Language for an Assignment  Homework 2
1932 words, about 10 minutes to read.
After the madness of the language for homework 1, the solution to the second homework offers a moment of respite. Let’s get right into the problems, shall we? ...

A Language for an Assignment  Homework 1
3918 words, about 19 minutes to read.
On a rainy Oregon day, I was walking between classes with a group of friends. We were discussing the various ways to obfuscate solutions to the weekly homework assignments in our Algorithms course: replace every if with a ternary expression, use single variable names, put everything on one line. ...