MarisaKirisame

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

swatson555

#!/usr/bin/env scheme --script

(import (nanopass))

(define unique-var
  (let ()
    (define count 0)
    (lambda (name)
      (let ([c count])
        (set! count (+ count 1))

shhyou

#lang racket/base

(require racket/match)

(provide current-solver-path
         call-with-solver
         solve)

(define current-solver-path (make-parameter (find-executable-path "z3")))

soegaard

#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.

MattPD

Program Analysis Resources

(draft; work in progress)

See also:

• Compilers
  • correctness
• Program analysis:
• Dynamic analysis - instrumentation, translation, sanitizers

andregrigon

How to Debug Chez Scheme Programs

R. Kent Dybvig

August 2002

1. Basic debugging techniques
   1. Kinds of failure
   2. Understanding error messages
   3. Staring at the code
2. Simplifying the code and input

soegaard

#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
    

paulcadman

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.

AndyShiue

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.

larvata

ffmpeg Cheatsheet

-loglevel debug

• Join TS Files
• Convert TS to MP4
• Download Online AES-128 Encrypted HLS video
• Convert Video to GIF