Skip to content

Instantly share code, notes, and snippets.

View csgordon's full-sized avatar

Colin S. Gordon csgordon

69 followers · 14 following
View GitHub Profile
@csgordon
csgordon / Dockerfile
Created April 1, 2021 17:25
Dockerfile for depccg
FROM ubuntu:focal-20200729
# Core stuff
ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update
# Apparently installing tzdata here explicitly avoids an interactive dialog later
RUN apt-get install -y apt-utils tzdata
RUN ln -sf /usr/share/zoneinfo/US/Eastern /etc/localtime
RUN dpkg-reconfigure -f noninteractive tzdata
#RUN ntpd -gq
@csgordon
csgordon / linux_hyperv.md
Created June 24, 2020 15:51

I've been running Linux in Hyper-V for some time, as an alternative to remotely connecting or dual-booting. A perpetual problem with this, however, is that Hyper-V's hyperv_fb driver only supports monitor resolutions up to 1600x1200, and doesn't support resizing. (Microsoft has guest extensions, but they are gradually maintained for fewer and fewer variants of Linux; currently it appears only RHEL is actively maintained, with the latest Ubuntu release supporting 18.04. It is now 2020.)

I've tried a number of different approaches to connecting remotely to a Hyper-V machine over the years, and most break after some period of time. I have a relatively stable solution for connecting to a Docker container with RDP, but if I want to run programs using lots of memory, I don't necessarily want to dedicate that much memory to the main Docker host VM.

The following short script is based on instructions I found for making it possible to SSH

@csgordon
csgordon / popl20response.md
Created September 19, 2019 15:24

Thank you for your reviews. After a shorter general response, there are point-by-point responses for those inclined to read them.

As far as motivation (Reviewer A): there are currently a range of interesting program analyses formulated as sequential effect systems. Currently, none of them can handle control flow more complicated than while loops or simple recursion. Exceptions and generators, which are now widespread, have never been addressed in any sequential effect system. While there is perhaps a case to be made that delimited continuations might be "more" than we should address directly (Reviewer B), it seems that growing interest in algebraic effects (tunneling algebraic effects are essentially tagged delimited continuations) and the impending addition of explicit delimited

@csgordon
csgordon / HybridAssertionsForActors.dfy
Created September 11, 2019 16:37
Prototyping Actor verification in Dafny
/*
* Sample code for the AGERE 2019 paper "Modal Assertions for Actor Correctness" by Colin S. Gordon, DOI 10.1145/3358499.3361221.
* Note that at the time of this writing, there is an issue (https://github.com/dafny-lang/dafny/issues/359) where this file only verifies from the command line (modulo complains about missing implementations of abstract methods). Currently, verifying this via the Dafny Visual Studio Code plugin runs into trouble with the higher-order predicates.
* Last checked with a local build of Dafny commit 8f141e9d05b2dba9de4ba997040df6166c2d168c and Boogie commit bc49937e7ee88e931bbe2dbf779a42612731a8fd
*/
module ActorCore {
class {:extern} ActorRef<Ms> {}
predicate {:extern} at<T,Ms>(i: ActorRef<Ms>, p:(T ~> bool))
@csgordon
csgordon / Actors.dfy
Created August 2, 2019 00:13
Partial axiomatization of hybrid logic assertions for actors in Dafny
module ActorCore {
class {:extern} ActorRef<Ms> {}
predicate {:extern} at<T,Ms>(i: ActorRef<Ms>, p:(T ~> bool))
/* at[i](_) is a modality */
lemma atImpl<T,M>(c:ActorRef<M>, P:T~>bool, Q:T~>bool)
requires forall x:T :: P.requires(x) ==> Q.requires(x)
requires forall x:T :: P.requires(x) ==> P(x) ==> Q(x)
ensures at(c, P) ==> at(c, Q)
/* When using the above, Dafny sometimes doesn't notice the precondition holds;
this variant forces it to look for it. */
@csgordon
csgordon / lang.v
Created June 12, 2019 02:40
OOPSLA'19 Paper 161 Coq 8.9.0 formalization of Figure 2, functions of Figure 3, and iteration
Require Import Utf8.
Require Import Program.
Require Import Arith.
Require Import Ensembles.
Require Import Setoid.
Require Import Relations.
Require Import Morphisms.
Require Import Coq.Classes.Equivalence.
Polymorphic Definition binop (E:Type) := E -> E -> E.
@csgordon
csgordon / arxivlog.txt
Created May 30, 2019 16:21
TeX log appears below
[verbose]: Creating arXiv submission AutoTeX object
[verbose]: *** Using TeX Live 2016 ***
[verbose]: Calling arXiv submission AutoTeX process
[verbose]: TeX/AutoTeX.pm: admin_timeout = minion
[verbose]: <acmart.cls> is of type 'TeX auxiliary'.
[verbose]: <journalarxiv.bbl> is of type 'TeX auxiliary'.
[verbose]: <journalarxiv.tex> is of type 'LATEX2e'.
[verbose]: ~~~~~~~~~~~ Processing file 'journalarxiv.tex'
@csgordon
csgordon / keybase.md
Created July 27, 2015 06:28

Keybase proof

I hereby claim:

  • I am csgordon on github.
  • I am csgordon (https://keybase.io/csgordon) on keybase.
  • I have a public key whose fingerprint is 31DF C618 06FE DE8D D007 7571 5A37 6FB7 4F95 CA41

To claim this, I am signing this object:

@csgordon
csgordon / StrictlyPositive.idr
Created September 9, 2013 18:47
Definition that isn't strictly positive according to Agda or Coq, but is accepted by Idris (:total ElimT says ElimT is total, which requires not using non-SP types)
data T : Type -> Type where
c1 : T Nat
c2 : T (T Nat)
ElimT : (A : Type) -> T A -> A
ElimT _ c1 = 3
ElimT _ c2 = c1
@csgordon
csgordon / LF.agda
Last active December 21, 2015 13:08
Nearly-complete inductive-recursive encoding of LF in Agda
open import Data.Nat
open import Data.Fin
open import Level
open import Relation.Binary.PropositionalEquality
module LF where
{- Semantic model primitives -}
Rℕ : {C : ℕ -> Set} -> (x : ℕ) -> C ℕ.zero -> ((n : ℕ) -> C n -> C (ℕ.suc n)) -> C x
Rℕ ℕ.zero z s = z