Pinned Repositories
cbpv-effects-coeffects
Formalization of CBPV extended with effect and coeffect tracking
cbpv-in-agda
Formalization of Call-By-Push-Value, augmented with effect tracking
cis670-16fa
Advanced Topics in Programming Languages, Penn CIS 670, Fall 2016
cis6700-23sp
CIS 6700, Spring 2023
dcoi-impl
A demo implementation of a dependent calculus of indistinguishability
hs-to-coq
Convert Haskell source code to Coq source code.
lngen
Tool for generating Locally Nameless definitions and proofs in Coq, working together with Ott
metalib
The Penn Locally Nameless Metatheory Library
plclub-web
A Hakyll [plclub] website (https://www.cis.upenn.edu/~plclub/)
StraTT
Supplementary material for Stratified Type Theory
The Penn PL Club's Repositories
plclub/hs-to-coq
Convert Haskell source code to Coq source code.
plclub/metalib
The Penn Locally Nameless Metatheory Library
plclub/cis670-16fa
Advanced Topics in Programming Languages, Penn CIS 670, Fall 2016
plclub/lngen
Tool for generating Locally Nameless definitions and proofs in Coq, working together with Ott
plclub/cis6700-23sp
CIS 6700, Spring 2023
plclub/plclub-web
A Hakyll [plclub] website (https://www.cis.upenn.edu/~plclub/)
plclub/cbpv-effects-coeffects
Formalization of CBPV extended with effect and coeffect tracking
plclub/cbpv-in-agda
Formalization of Call-By-Push-Value, augmented with effect tracking
plclub/dcoi-impl
A demo implementation of a dependent calculus of indistinguishability
plclub/StraTT
Supplementary material for Stratified Type Theory
plclub/plclub-web-old
Old PLClub website git mirror. Retired Jan 15 2020.