❄️ All Configurations for My Laptop

Mechanizations of Type Theories

Practising Normalization by Evaluation on STLC.

Elixir is a dynamic, functional language for building scalable and maintainable applications

🤖 Just a command runner

📅 A clean and elegant calender with date links

Multitier JavaScript

🍔 Chen’s Private Cuisine Menu

A demo implementation of a simple dependently-typed language

Display and control your Android device

Artifact for paper "When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism" (https://popl24.sigplan.org/details/POPL-2024-popl-research-papers/50)

A Toy Inverse Bidirectional Typechecker

Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization

Coq formalization of System Fcc (coercion framework)

A list of various lists consisting of academics on Mastodon

A minimalist Jekyll theme for running a blog or publication powered by Jekyll and GitHub Pages

An inarguably well-designed Jekyll theme.

The open Master Hearing Aid (openMHA)

The Coq proofs of my dissertation "Iso-Recursive Subtyping: New Theory and Extensions"

The Ott tool for writing definitions of programming languages and calculi

The Next Generation of Compositional Programming

Formal development of a type-safe intermediate language for tensor expressions.

A document language for the browser

A reflection-based proof tactic for lattices in Coq

Tricks you wish the Coq manual told you [maintainer=@tchajed]