kini

[foo*]
indent_size = 2

[foobar*]
indent_size = unset

kini

  ;; ACL2 certification dimmer function
  (defun acl2-cert-dimmer-for-comint (str)
    "When cert.pl says it has certified something, go back and
dim the text where it said it was making that thing.  This way
you can easily tell at a glance what books are still certifying."
    (let ((pos-in-str nil)
          ;; This is broken; comint-last-input-end isn't really the
          ;; end of the last input.  I should probably search to the
          ;; previous prompt, or something.
          (beginning-of-output comint-last-input-end))

kini

@article{greenwade93,
    author  = "George D. Greenwade",
    title   = "The {C}omprehensive {T}ex {A}rchive {N}etwork ({CTAN})",
    year    = "1993",
    journal = "TUGBoat",
    volume  = "14",
    number  = "3",
    pages   = "342--351"
}

kini

#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#include <stdbool.h>

bool print_permutation(unsigned int n,
                       unsigned int permutation[n],
                       unsigned int count[n]) {
  printf("Permutation: [");
  for (unsigned int i = 0; i < n; i++) {

kini

random () {
    # note: $RANDOM only gives 15 bits of entropy, and the apparently
    # commonly used $RANDOM$RANDOM is non-uniform as it misses such
    # numbers as 4294967295.  This command will grab 4 bytes from
    # /dev/urandom, interpret them as a 4-byte unsigned integer, and
    # format them in decimal representation.  It can be used as a
    # replacement for $RANDOM when you want a full 32 bits of entropy.
    od -An -t u4 -N4 < /dev/urandom | tr -d '[[:space:]]'
}
export -f random

kini

Compiler Lab: Generating Assembly Code

Introduction

• Assigned: Oct. 14
• Due: Oct. 30, 11:59 PM

Note: Keshav Kini ([email protected]) is the lead TA for this lab assignment.

kini

Bomb Lab: Defusing a Binary Bomb

Introduction

• Assigned: Sep. 28
• Due: Oct. 12

Note: Keshav Kini ([email protected]) is the lead TA for this lab assignment.

kini

ReverseLike in ACL2 with constrained functions

This document describes a toy example of how ACL2’s “constrained functions” feature can be used to verify some higher-order statements, despite ACL2 being a first-order theorem prover.

Suppose we have a function called $reverse$ which when applied to a list returns a list containing the same elements in reverse order. Consider the following proposition.

kini

Keybase proof

I hereby claim:

• I am kini on github.
• I am kini (https://keybase.io/kini) on keybase.
• I have a public key whose fingerprint is 75ED 46F8 A0C4 C645 32AB B79D 7492 7B7C A81A 950F

To claim this, I am signing this object:

kini

#!/bin/bash

set -ex

PACKAGE="$1"
DEPENDENCY="$2"
TMPDIR="$(mktemp -d)"

pushd "$TMPDIR"
cabal get --pristine "$PACKAGE"