Skip to content

Instantly share code, notes, and snippets.

Ayberk Tosun ayberkt

View GitHub Profile
View Problem.agda
{-# OPTIONS --cubical --safe #-}
module Problem where
open import Cubical.Core.Everything using ( _≡_
; Type
; Σ
; Σ-syntax
; _,_ )
open import Cubical.Data.Prod using ( _,_; proj₁; proj₂ )
View 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 17AA 88FB 333F F93A 4C3A 2531 2409 CCD7 6D12 4F2B

To claim this, I am signing this object:

View 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:

View id_rsa.pub
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 Aug 28, 2017
GF Documentation Pointers
View gf-resources.md
View 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 Jul 21, 2017
Code from Harper's Proof-Directed Debugging
View regexp.sml
structure Regex =
struct
datatype regexp =
Zero
| One
| Char of char
| Times of regexp * regexp
| Plus of regexp * regexp
| Star of regexp
View equilibrium.scm
(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 Dec 7, 2015
Makefile for LaTeX
View Makefile
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
You can’t perform that action at this time.