Beluga and explicit contexts

:: research, notes

In my recent work, I found it useful to pair a term and its context in order to more easily reason about weakening the context. At the prompting of a colleague, I’ve been reading about Beluga, [1] [2], and their support for programming with explicit contexts. The idea seems neat, but I’m not quite sure I understand the motivations or implications.

So it seems Beluga has support for describing what a context contains (schemas), describing in which context a type/term is valid, and referring to the variables in a context by name without explicitly worrying about alpha-renaming. This technique supports reasoning about binders with HOAS in more settings, such as in the presence of open data and dependent types. Since HOAS simplifies reasoning about binders by taking advantage of the underlying language’s implementation of substitutions, this can greatly simplify formalized meta-theory in the presence of advanced features which previously required formalizing binders using more complicated techniques like De Bruijn indices. By including weakening, meta-variables, and parameter variables, Beluga enables meta-theory proofs involving binders to be much more natural, i.e., closer to pen-and-paper proofs.

Obviously this is great for formalized meta-theory. While I have seen how HOAS can simplify life for the meta-theorist, and seen how it fails, I don’t fully understand the strengths and weakness of this work, or how it compares to techniques such as the locally nameless. I’m also not sure if there is more to this work than a better way to handle formalization of binding (which is a fine, useful accomplishment by itself).

If anyone can elaborate on or correct my understanding, please do.

An on demand Minecraft Server

:: games, tricks, linux

Sometimes I play minecraft. Sometimes I play a lot of minecraft and sometimes I just stop playing for months. Lately when I do play, I’ve bene playing with a slightly modified version of Tekkit and running my own server. I have a VPS that I probably under use, so I decided to run the server there for when I do play with my friends.

My VPS is not very powerful, and running a Minecraft server when I stop playing for months is a huge waste of resources. I sought a way to automatically bring the server up when I wanted to play and shut it down when I wasn’t playing for a while.

To be or not to be … paranoid.

:: musings

I wear my tinfoil hat proudly. I block ads, and JavaScript, and tracking cookies. I use HTTPS everywhere, I encrypt all my hard drives, I used randomly generated passwords, and I would encrypt all my emails if anyone else bothered to use GPG. I even run my own mail server, and have been considering running my own CalDAV and CardDAV server ...

But lately, I’ve been thinking maybe I should allow some ads and tracking, and let Google or Apple manage some of my data.

A test post in Frog

:: meta

I’m converting my blog and website to Frog/Scribble.

This is my first post.

I like it better than Octopress. I get Racket and Scribble for templating, Markdown or Scribble support for blogging and pages, and I don’t need Ruby. The conversion process was dead simple, given that Octopress posts were already in Markdown.

FASTR

:: open access, research, academia

FASTR is a bill to ensure all publically funded research is open access. I urge you all to contact your congresspeople and demand they support this bill.

A new blog

:: meta

I finally switched my blog from WordPress. Despite my aversion to ruby, I went with Octopress. It’s a little easier to work with and has a slightly nicer default infrastructure.

Using Evil for Good

:: linux, tricks

So I use Vim as my primary editor. Unfortunately, some applications I require (e.g. Proof General) run only on the Emacs operation system, which comes with a terrible editor. Thankfully, I’ve found a pretty decent port of Vim to Emacs, called (appropriately) Evil.