Skip to content
@plclub

The Penn PL Club

Popular repositories Loading

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

    Convert Haskell source code to Coq source code.

    Coq 93 11

  2. metalib metalib Public

    The Penn Locally Nameless Metatheory Library

    Coq 76 24

  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 14

Repositories

Showing 10 of 12 repositories
  • StraTT Public Forked from sweirich/pi-forall

    Supplementary material for Stratified Type Theory

    plclub/StraTT’s past year of commit activity
    Haskell 6 Zlib 99 0 0 Updated Jan 20, 2026
  • plclub-web Public

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

    plclub/plclub-web’s past year of commit activity
    HTML 6 19 8 (3 issues need help) 0 Updated Jan 9, 2026
  • typing-strictness Public

    Formalization of the proofs in the POPL 2026 paper Typing Strictness

    plclub/typing-strictness’s past year of commit activity
    Rocq Prover 6 BSD-2-Clause 0 0 0 Updated Nov 14, 2025
  • hs-to-coq Public

    Convert Haskell source code to Coq source code.

    plclub/hs-to-coq’s past year of commit activity
    Coq 93 MIT 11 55 4 Updated Jun 24, 2025
  • metalib Public

    The Penn Locally Nameless Metatheory Library

    plclub/metalib’s past year of commit activity
    Coq 76 24 2 1 Updated Mar 26, 2025
  • lngen Public

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

    plclub/lngen’s past year of commit activity
    Haskell 32 MIT 8 0 0 Updated Oct 22, 2024
  • cbpv-effects-coeffects Public

    Formalization of CBPV extended with effect and coeffect tracking

    plclub/cbpv-effects-coeffects’s past year of commit activity
    Coq 14 BSD-2-Clause 0 0 0 Updated Aug 30, 2024
  • dcoi-impl Public Forked from sweirich/pi-forall

    A demo implementation of a dependent calculus of indistinguishability

    plclub/dcoi-impl’s past year of commit activity
    Haskell 2 BSD-3-Clause 99 0 0 Updated May 27, 2024
  • cbpv-in-agda Public

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

    plclub/cbpv-in-agda’s past year of commit activity
    Agda 3 1 0 0 Updated Nov 24, 2023
  • cis6700-23sp Public

    CIS 6700, Spring 2023

    plclub/cis6700-23sp’s past year of commit activity
    Agda 18 MIT 1 0 0 Updated Feb 15, 2023
View all repositories

Most used topics

Loading…