Popular repositories Loading

1. hs-to-coq hs-to-coq Public

   Convert Haskell source code to Coq source code.

   Coq 85 9

2. metalib metalib Public

   The Penn Locally Nameless Metatheory Library

   Coq 74 23

3. cis670-16fa cis670-16fa Public

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

   Coq 42 10

4. lngen lngen Public

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

   Haskell 32 8

5. cis6700-23sp cis6700-23sp Public

   CIS 6700, Spring 2023

   Agda 18 1

6. cbpv-effects-coeffects cbpv-effects-coeffects Public

   Formalization of CBPV extended with effect and coeffect tracking

   Coq 12