philnguyen

(define (f x)
  ;; implicit recursive call to `f` not instrumented by the library
  (with-handlers ([number? f])
     (raise (add1 x))))
     
(begin/termination (f 0))

philnguyen

(module lib racket
  (provide
   (contract-out
    ;; old model didn't have integer division
    [quotient (->i ([n (and/c integer? (>=/c 0))])
                   (res (n) (->i ([d (and/c integer? (>/c 0))])
                                 (res (d) (and/c integer?
                                                 (>=/c 0)
                                                 (λ (r) (<= (* r d) n)))))))]
    [length ((listof any/c) . -> . (and/c integer? (>=/c 0)))]

philnguyen

(define L
  (λ (x)
    (cond
      ;; `x` is higher order
      [(proc? x)
       (cond ;; Send message `L_x` to `x` and transfer controll to `L_f`, with `L_f`'s shape to be decided
             [L_1 ((L_f (x L_x)) x)]
             ;; Return closure referencing `x`, with `L_g`'s shape to be decided
             ;; Shu-Hung pointed out that this case was redundant
             ;; [L_2 (λ (y) ((L_g x) y))]

philnguyen

#lang typed/racket/base

(require racket/match
         racket/list
         racket/set
         bnf)

(Color     . ⩴ . 'green 'yellow 'black 'brown 'red 'pink 'blue)
(Name      . ≜ . Symbol)
(Piece     . ≜ . (Piece [digit : Integer] [color : Color]) #:ad-hoc)

philnguyen

#lang racket/base

(require racket/contract
         racket/set
         racket/match
         redex)

(define-language L
  ;; Syntax
  ;; λ-calculus extended with:

philnguyen

#lang racket/base
(require racket/match
         racket/contract
         racket/list
         racket/function
         (only-in typed/racket/base assert))

;; Assume primitive `induct-on` that can inspect contracts
;; and produce induction principles for *some* contracts
;; deemed to specify inductive data

philnguyen

#lang racket/base

(require racket/set
         racket/list
         racket/match
         racket/syntax
         redex)

(define-language L
  ;; Syntax

philnguyen

;; Module `main` requires an identifier from module `helper-1.rkt` without `fake-contract` in there
(module main racket
  (#%module-begin
   (module configure-runtime '#%kernel
     (#%module-begin (#%require racket/runtime-config) (#%app configure '#f)))
   (#%require soft-contract/fake-contract)
   (#%require helper-1.rkt)
   (define-values
    (lifted.0)
    (#%app

philnguyen

;; Module `main` requires an identifier from module `helper-1.rkt` with `fake-contract` in there
(module main racket
  (#%module-begin
   (module configure-runtime '#%kernel
     (#%module-begin (#%require racket/runtime-config) (#%app configure '#f)))
   (#%require soft-contract/fake-contract)
   (#%require helper-1.rkt)
   (define-values
    (lifted.0)
    (begin

philnguyen

#lang typed/racket

(require z3/ffi
         z3/smt)

;; Example of how to use Z3-Model in current Racket Z3 library.
;; The common pattern in extracting data with the low-level Z3 library is
;; - querying how many things are there
;; - getting the ith "key" and "value"
;; Some functions used in the following example: