Skip to content

Instantly share code, notes, and snippets.

View ayberkt's full-sized avatar

Ayberk Tosun ayberkt

View GitHub Profile
{-# OPTIONS --cubical --safe #-}
module Problem where
open import Cubical.Core.Everything using ( _≡_
; Type
; Σ
; Σ-syntax
; _,_ )
open import Cubical.Data.Prod using ( _,_; proj₁; proj₂ )

Keybase proof

I hereby claim:

  • I am ayberkt on github.
  • I am ayberkt (https://keybase.io/ayberkt) on keybase.
  • I have a public key whose fingerprint is 17AA 88FB 333F F93A 4C3A 2531 2409 CCD7 6D12 4F2B

To claim this, I am signing this object:

@ayberkt
ayberkt / keybase.md
Last active October 4, 2017 18:53
keybase.md

Keybase proof

I hereby claim:

  • I am ayberkt on github.
  • I am ayberkt (https://keybase.io/ayberkt) on keybase.
  • I have a public key whose fingerprint is 6DB0 41EE 6BA4 C35C 5E31 0A54 3F60 CB76 1EB4 7FD7

To claim this, I am signing this object:

@ayberkt
ayberkt / id_rsa.pub
Created October 4, 2017 16:29
Public RSA key
ssh-rsa AAAAB3NzaC1yc2EAAAADAQABAAABAQDB/ThJZfpaHI337U5cq56ydyg8PuoYUYfxgRkbHTIq24JLO49x6YxsyaFL2cqHZwmzLMuMQrGtOlznnc+Ud88ni6nfgHX1zztNNFZ6EzUXsEKIXqqmuQEGXWg1pLuMMRjB6qaG781K3Lrd3yjmXA8+f5/+3aLAv85cy+tVeZsF8dyAhyBq75wLj1E2kNfBcqBbZkGek4UgzSL/9MqgtTQp9vWAPpR+d8RznIf79iZo0sPmNyW0nOzPFJiMbOcbN8fEChPQv3xGM7AWzdCxY+hGlnqk/Ki3b4+7rmZ5a+j+NqLogmMABeSwwdmDzWRvUKt/yzsZ9KNAfJqZTCTfChNd tosun2@illinois.edu
@ayberkt
ayberkt / gf-resources.md
Created August 28, 2017 18:48
GF Documentation Pointers
@ayberkt
ayberkt / CityTur.gf
Last active August 15, 2017 08:44
CityTur.gf
concrete CityTur of City = open Prelude in {
flags
lexer=bind;
param
WowelType = Front | Back;
DefAccCase = OnlyI WowelType | SoftenCons WowelType | InsertY WowelType;
lincat
Phrase = Str;
@ayberkt
ayberkt / regexp.sml
Created July 21, 2017 23:35
Code from Harper's Proof-Directed Debugging
structure Regex =
struct
datatype regexp =
Zero
| One
| Char of char
| Times of regexp * regexp
| Plus of regexp * regexp
| Star of regexp
(define-fun is-prob ((r Real)) Bool (and (>= r 0) (<= r 1)))
(define-fun equi ((a Real) (b Real) (c Real) (d Real) (r Real) (s Real)) Real
(+ (* r s a) (* r (- 1 s) b) (* (- 1 r) s c) (* (- 1 r) (- 1 s) d)))
(assert
(forall ((x1 Real) (y1 Real) (w1 Real) (z1 Real)
(x2 Real) (y2 Real) (w2 Real) (z2 Real))
(exists ((r Real) (s Real))
(=>
@ayberkt
ayberkt / Makefile
Last active December 7, 2015 20:42
Makefile for LaTeX
all:
pdflatex paper.tex
bib:
latex paper.tex && bibtex paper.aux && latex paper.tex && pdflatex paper.tex
clean:
rm -f paper.pdf
rm -f paper.aux
rm -f paper.log