Repositories list

• LambdaIFCStar

  Public
  The Agda mechanization of a gradual security-typed programming language with general mutable references.

  semanticsagdaformalization+ 6coercionmeta-theorygradual-typinginformation-flowtype-systemsnoninterference

  Agda

  •1•4•0•0•Updated May 24, 2024May 24, 2024

• lambda-sec

  Public archive
  Agda

  •0•0•0•0•Updated Jan 26, 2023Jan 26, 2023

• Grift

  Public
  A compiler for the gradually typed lambda calculus

  compilergradual-typinggrift

  C

  •

  MIT License

  •11•76•26•3•Updated Nov 4, 2021Nov 4, 2021

• Dynamizer

  Public
  Dynamizer produces valid less precisely-typed versions of a valid program in Grift.

  Haskell

  •

  GNU General Public License v3.0

  •1•1•0•0•Updated Sep 30, 2021Sep 30, 2021

• Equivalence-of-Cast-Calculi

  Public
  Agda

  •1•0•0•0•Updated Nov 29, 2020Nov 29, 2020

• benchmarks

  Public
  Collection of benchmarks for gradually-typed languages

  benchmarksgradual-typing

  Racket

  •2•4•3•0•Updated Apr 25, 2020Apr 25, 2020

• Reversible-Hypercoercions

  Public
  Useful in mutable references.

  Agda

  •0•0•0•0•Updated Nov 8, 2019Nov 8, 2019

• language-grift

  Public
  Parser and pretty printer for Grift languages

  Haskell

  •

  BSD 3-Clause "New" or "Revised" License

  •0•1•0•0•Updated Feb 25, 2019Feb 25, 2019

• gtp-benchmarks

  Public
  Gradual Typing Performance benchmarks

  Racket

  •

  Other

  •11•0•0•0•Updated Nov 13, 2018Nov 13, 2018

• gtp

  Public
  NSF grant website

  HTML

  •3•0•0•0•Updated Oct 2, 2018Oct 2, 2018

• gradual-guarantee-proofs

  Public
  Dockerfile

  •0•0•0•0•Updated Sep 1, 2018Sep 1, 2018

• toys

  Public
  An repository for collecting experiments that explore semantic choices with interpreters and models.

  Racket

  •

  MIT License

  •0•1•0•0•Updated Mar 27, 2018Mar 27, 2018