kmicinski

(define (synthesize-type env e)
  (match e
    ;; Literals
    [(? integer? i) 'int]
    [(? boolean? b) 'bool]
    ;; Look up a type variable in an environment
    [(? symbol? x) (hash-ref env x)]
    ;; Lambda w/ annotation
    [`(lambda (,x : ,A) ,e)
     ;; I know the type is A -> B, where B is the type of e when I

kmicinski

#lang racket

(define (op? op)
  (member op '(+ - * / cons car cdr = equal? length)))

(define (op->racket op)
  (eval op (make-base-namespace))) ;; the *only* acceptable use of Racket's `eval` in this project

;; First attempt
(define (eval-a e env)

kmicinski

#lang racket

(define (expr? e)
  (match e
    [(? number? n) #t]
    [(? symbol? x) #t]
    [`(λ (,(? symbol? x)) ,(? expr? e)) #t]
    [`(,(? expr? e0) ,(? expr? e1)) #t]
    [_ #f]))

kmicinski

#lang racket

;; general direct-style recursive template over lists
#;(define (my-function lst)
  (if (empty? lst)
      'base-case
      (let ([result-from-rest-of-list (my-function (rest lst))]
            [first-list (first lst)])
        (f first-list result-from-rest-of-list))))

kmicinski

#lang racket

;; omega term = 
;; ((lambda (x) (x x)) (lambda (x) (x x)))
;; (x x) [ x ↦ (lambda (x) (x x)) ] =
;; ((lambda (x) (x x)) (lambda (x) (x x)))

;; there are two options
'((lambda (x) (lambda (y) y)) ((lambda (x) (x x)) (lambda (x) (x x))))

kmicinski

#lang racket

;; λ-calculus expressions
(define (expr? e)
  (match e
    [(? symbol? x) #t] ;; variables
    [`(λ (,(? symbol? x)) ,(? expr? e-body)) #t] ;; λ abstractions
    [`(,(? expr? e-f) ,(? expr? e-a)) #t] ;; applications
    [_ #f]))

kmicinski

#lang racket

;; CIS700, Fall 2023 -- Kris Micinski
;; 
;; Demo of SMT (SMTLIB) to perform bounded-model checking for an example
;; program.
;; 
;;  // input x, a bit vector of length N
;;  i = 0;
;;  r = 0;

kmicinski

;; CIS352 -- Fall 2023
;; Closure-Creating Interpreters
#lang racket

(define (expr? e)
  (match e
    [(? symbol? x) #t] ;; variables
    [(? number? n) #t]
    ;; single-variable let binding
    [`(let ([,(? symbol? x) ,(? expr? e-let-binding)]) ,(? expr? e-body)) #t]

kmicinski

#lang racket

;; CIS352 Office hours code -- 9/27/2023
;; matching and type predicates

;; Direct-style length
(define (length lst)
  (if (empty? lst)
      0
      (add1 (length (rest lst)))))

kmicinski

#lang racket

;; CIS352 -- Fall 2023
;; Lambdas

;; first order function -- no functions as arguments
;; O(n^2) the way it's written -- an easier implementation
;; is not easy functionally, need a different representation 
(define (reverse lst)
  (if (empty? lst)