PLT research

This repository contains several PLT related sub-projects that I created for learning these certain subjects.

• the little typer note
• continuation
• lambda calculus
  • utlc: untyped lambda calculus
  • stlc: simply typed lambda calculus
  • de-bruijn index is a technology to encode variables by indcies
• polymorphism
  • hindley milner is a classic decidable algorithm and polymorphic type system variant
  • row polymorphism is a type system that you can have record row polymorphic, but my code is buggy
• dependent type
  • lambda pi introduces $\Pi$ type
  • strictly positive is an attribute that well inductive data type should hold, and this is a syntactic checker for it
  • universe polymorphism
  • normalization by evaluation
  • elaboration-zoo
    • whisper: conversion check
    • antaa: meta solving
• external
  • Write you a programming language

Compiler

Here are works that more about implementation/assembly details

1. racket-llvm
2. still compiling
3. scheme to arm64
4. c to x64
5. little-scheme: A little scheme interpreter for playing SICP
6. elz

NOTE: video

• Kent Dybvig: Macro-Writer’s Bill of Rights
• “Let’s Build a Hygienic Macro Expander” by Matthew Flatt