Repositories list

• lngen

  Public
  Tool for generating Locally Nameless definitions and proofs in Coq, working together with Ott

  Haskell

  •

  MIT License

  •9•30•0•0•Updated Oct 22, 2024Oct 22, 2024

• StraTT

  Public
  Supplementary material for Stratified Type Theory

  Haskell

  •

  zlib License

  •89•1•0•0•Updated Oct 20, 2024Oct 20, 2024

• plclub-web

  Public
  A Hakyll [plclub] website (https://www.cis.upenn.edu/~plclub/)

  HTML

  •19•6•8•0•Updated Sep 5, 2024Sep 5, 2024

• cbpv-effects-coeffects

  Public
  Formalization of CBPV extended with effect and coeffect tracking

  Coq

  •

  BSD 2-Clause "Simplified" License

  •0•11•0•0•Updated Aug 30, 2024Aug 30, 2024

• hs-to-coq

  Public
  Convert Haskell source code to Coq source code.

  haskellcoq

  Coq

  •

  MIT License

  •8•78•54•3•Updated Aug 27, 2024Aug 27, 2024

• metalib

  Public
  The Penn Locally Nameless Metatheory Library

  Coq

  •

  Other

  •23•71•2•2•Updated Jun 23, 2024Jun 23, 2024

• dcoi-impl

  Public
  A demo implementation of a dependent calculus of indistinguishability

  Haskell

  •

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

  •89•2•0•0•Updated May 27, 2024May 27, 2024

• cbpv-in-agda

  Public
  Formalization of Call-By-Push-Value, augmented with effect tracking

  Agda

  •1•2•0•0•Updated Nov 24, 2023Nov 24, 2023

• cis6700-23sp

  Public
  CIS 6700, Spring 2023

  Agda

  •

  MIT License

  •1•15•0•0•Updated Feb 15, 2023Feb 15, 2023

• cis670-16fa

  Public
  Advanced Topics in Programming Languages, Penn CIS 670, Fall 2016

  Coq

  •

  MIT License

  •10•42•0•0•Updated Oct 25, 2022Oct 25, 2022

• plclub-web-old

  Public
  Old PLClub website git mirror. Retired Jan 15 2020.

  PHP

  •0•0•1•0•Updated Nov 14, 2019Nov 14, 2019