mietek

module Prime where

open import Codata.Musical.Notation
  using (∞ ; ♯_ ; ♭)

open import Codata.Musical.Stream
  using (_∷_ ; Stream)

open import Data.Empty
  using (⊥ ; ⊥-elim)

mietek

OAT COOKIES v1.0

rehydrate 1 cup raisins
melt 1/2 pack salted butter
prepare large mixing bowl

add 2 cups white sugar
add 1 table spoon ground cinnamon
add 1/2 cup whole milk
add 1/2 pack melted salted butter

mietek

Set up L2TP/IPsec VPN on Debian

Set up IPsec

Set up networking

mietek

On the Löbian obstacle

Miëtek Bak

Please see “Strongly-normalising agents” for a follow-up.

Throughout much of MIRI research work, there is an underlying assumption that a consistent system cannot prove its own consistency.

While it is usually acknowledged that the above assumption applies only to systems as strong as Peano Arithmetic (PA), it is done only in passing, with little consideration for the possibility of using other systems. Girard’s system F appears merely as a footnote, while Willard’s self-verifying systems merit just a brief mention. (YH2013, pp.6,9,18; F2013a, p.1; F2013b, p.1; FS2014, pp.3; FS2015, p.4b)

mietek

-- To simplify defining ChurchSigma.
{-# OPTIONS --type-in-type #-}

module Sigma where

open import Axiom.Extensionality.Propositional using (Extensionality)
open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; module ≡-Reasoning)
open ≡-Reasoning

mietek

open import Agda.Builtin.Equality using (_≡_ ; refl)

infixl 9 _&_
_&_ : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x x′} → x ≡ x′ → f x ≡ f x′
f & refl = refl

infixl 8 _⊗_
_⊗_ : ∀ {a b} {A : Set a} {B : Set b} {f f′ : A → B} {x x′} →
      f ≡ f′ → x ≡ x′ → f x ≡ f′ x′

mietek

module Choose where

open import Data.Product using (_,_ ; proj₁ ; proj₂ ; ∃) renaming (_×_ to _∧_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; sym ; subst)
open import Relation.Nullary using (¬_)

infix 0 _⇔_
_⇔_ : Set → Set → Set
A ⇔ B = (A → B) ∧ (B → A)

mietek

(defun lapply (fn x a)
  (cond ((atom fn) (cond ((eq fn 'car) (caar x))
                         ((eq fn 'cdr) (cdar x))
                         ((eq fn 'cons) (cons (car x) (cadr x)))
                         ((eq fn 'atom) (atom (car x)))
                         ((eq fn 'eq) (eq (car x) (cadr x)))
                         ((eq fn 'read) (read))
                         (t (lapply (leval fn a) x a))))
        ((eq (car fn) 'lambda) (leval (caddr fn) (pairlis (cadr fn) x a)))
        ((eq (car fn) 'label) (lapply (caddr fn) (cons (cons (cadr fn)

mietek

module DataCodata where

open import Data.Product using (_×_ ; _,_)
open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)


--------------------------------------------------------------------------------


case : ∀ {ℓ ℓ′ ℓ″} → {X : Set ℓ} {Y : Set ℓ′} {Z : Set ℓ″}

mietek

#!/usr/bin/env bash

set -eu

declare _R         # Return register

declare -i _F=0    # Current frame

declare -a _S=()   # Stack frame data
declare -i _SP=0   # Beginning of current stack frame