(draft; work in progress)
See also:
- Compilers
- Program analysis:
- Dynamic analysis - instrumentation, translation, sanitizers
type expr = | |
| Var of string | |
| Int of int | |
| Add of (expr * expr) | |
| Mult of (expr * expr) | |
| Let of (string * expr * expr) | |
| IfZero of (expr * expr * expr) | |
| Pair of (expr * expr) | |
| Zro of expr | |
| Fst of expr |
#!/usr/bin/env scheme --script | |
(import (nanopass)) | |
(define unique-var | |
(let () | |
(define count 0) | |
(lambda (name) | |
(let ([c count]) | |
(set! count (+ count 1)) |
#lang racket/base | |
(require racket/match) | |
(provide current-solver-path | |
call-with-solver | |
solve) | |
(define current-solver-path (make-parameter (find-executable-path "z3"))) |
#lang racket/base | |
(provide uniq) | |
;;; | |
;;; Uniq | |
;;; | |
; The function uniq takes a list as input and returns a new list: | |
; adjacent elements are compared and omits any repeated elements. | |
; In other words, uniq works like the Unix utility uniq, but on list. |
(draft; work in progress)
See also:
#lang racket | |
;; adapted from: | |
;; https://planet.racket-lang.org/package-source/dyoo/sicp-concurrency.plt/1/2/sicp-concurrency.ss | |
;; concurrency: SICP concurrency primitives | |
;; adapted from http://list.cs.brown.edu/pipermail/plt-scheme/2002-September/000620.html | |
;;; Sources: | |
;;; Dorai Sitaram, "Learn Scheme in a Fixnum of Dayes", chapter 15 | |
;;; Dyvig, http://www.scheme.com/tspl2d/examples.html#g2433 | |
Types are theorems, programs are proofs.
(The code examples here use idris https://www.idris-lang.org)
To augment testing with a finite number of inputs we write mathematical proofs that demonstrate their correctness on all possible inputs.
The programmer writes the proofs and the compiler checks the proofs as it builds the software.
I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.
Q: What is cubical type theory?
A: It’s a type theory giving homotopy type theory its computational meaning.
Q: What is homotopy type theory then?
A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.