Daniel's Blog

Tagged "Programming Languages"

• Implementing and Verifying "Static Program Analysis" in Agda, Part 7: Connecting Semantics and Control Flow Graphs

  4192 words, about 20 minutes to read.

  In the previous two posts, I covered two ways of looking at programs in my little toy language: In part 5, I covered the formal semantics of the programming language. ...

• Implementing and Verifying "Static Program Analysis" in Agda, Part 6: Control Flow Graphs

  3660 words, about 18 minutes to read.

  In the previous section, I’ve given a formal definition of the programming language that I’ve been trying to analyze. This formal definition serves as the “ground truth” for how our little imperative programs are executed; however, program analyses (especially in practice) seldom take the formal semantics as input. ...

• Implementing and Verifying "Static Program Analysis" in Agda, Part 5: Our Programming Language

  3794 words, about 18 minutes to read.

  In the previous several posts, I’ve formalized the notion of lattices, which are an essential ingredient to formalizing the analyses in Anders Møller’s lecture notes. ...

• Implementing and Verifying "Static Program Analysis" in Agda, Part 4: The Fixed-Point Algorithm

  2308 words, about 11 minutes to read.

  In the preivous post we looked at lattices of finite height, which are a crucial ingredient to our static analyses. In this post, I will describe the specific algorithm that makes use of these lattices; this algorithm will be at the core of this series. ...

• Implementing and Verifying "Static Program Analysis" in Agda, Part 3: Lattices of Finite Height

  7172 words, about 34 minutes to read.

  In the previous post, I introduced the class of finite-height lattices: lattices where chains made from elements and the less-than operator < can only be so long. ...

• Implementing and Verifying "Static Program Analysis" in Agda, Part 2: Combining Lattices

  5430 words, about 26 minutes to read.

  In the previous post, I wrote about how lattices arise when tracking, comparing and combining static information about programs. I then showed two simple lattices: the natural numbers, and the (parameterized) “above-below” lattice, which modified an arbitrary set with “bottom” and “top” elements ($\bot$ and $\top$ respectively). ...

• 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

  864 words, about 5 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 mini-language. ...

• 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. ...