A comprehensive collection of skills for Programming Languages research and development.
These skills were generated by LLMs and may contain hallucinations, factual errors, or incorrect references. Manual verification is in progress.
| abstract-interpretation-engine ❌ | abstract-machine ❌ | acsl-annotation-assistant ✅ | actor-model-implementer ❌ | algebraic-effects ❌ | alias-and-points-to-analysis ❌ |
| axiomatic-semantics ❌ | bidirectional-type-checking ❌ | bisimulation-checker ❌ | capability-system ❌ | closure-converter ❌ | common-subexpression-eliminator ❌ |
| concurrency-verifier ❌ | constant-propagation-pass ❌ | contextual-equivalence ❌ | control-flow-analysis ❌ | coq-proof-assistant ❌ | cps-transformer ❌ |
| dafny-verifier ❌ | dataflow-analysis-framework ❌ | dead-code-eliminator ❌ | defunctionalization ❌ | denotational-semantics-builder ❌ | dependent-type-implementer ❌ |
| dsl-embedding ❌ | effect-handlers-implementer ❌ | effect-system ❌ | effect-type-system ❌ | escape-analysis ❌ | existential-types ❌ |
| ffi-designer ❌ | fuzzer-generator ❌ | gadt-implementer ❌ | garbage-collector-implementer ❌ | graalvm-truffle-implementer ❌ | gradual-typing-implementer ❌ |
| higher-order-abstract-syntax ❌ | hoare-logic-verifier ❌ | incremental-computation ❌ | information-flow-analyzer ❌ | inline-expander ❌ | interprocedural-analysis ❌ |
| invariant-generator ❌ | jit-compiler-builder ❌ | lambda-calculus-interpreter ❌ | language-server-protocol ❌ | lean-prover ❌ | lexer-generator ❌ |
| linear-type-implementer ❌ | liveness-analysis ❌ | llvm-backend-generator ❌ | lock-free-data-structure ❌ | loop-optimizer ❌ | loop-termination-prover ❌ |
| macro-expander ❌ | memory-allocator ❌ | message-passing-system ❌ | mlir-dialect-designer ❌ | model-checker ❌ | module-system ❌ |
| monad-transformer ❌ | multi-stage-programming ❌ | operational-semantics-definer ❌ | ownership-type-system ❌ | parser-generator ❌ | partial-evaluator ❌ |
| polymorphic-effects ❌ | program-transformer ❌ | property-based-tester ❌ | race-detection-tool ❌ | reduction-semantics ❌ | refinement-type-checker ❌ |
| register-allocator ❌ | relational-parametricity-prover ❌ | row-polymorphism ❌ | rust-borrow-checker ❌ | sandbox-builder ❌ | separation-logician ❌ |
| session-type-checker ❌ | shape-analysis ❌ | simply-typed-lambda-calculus ❌ | smt-solver-interface ❌ | software-transactional-memory ❌ | ssa-constructor ❌ |
| subtyping-verifier ❌ | symbolic-execution-engine ❌ | system-f ❌ | taint-analysis ❌ | transactional-memory ❌ | type-checker-generator ❌ |
| type-class-implementer ❌ | type-directed-name-resolution ❌ | type-inference-engine ❌ | typed-assembly-language ❌ | value-analysis ❌ | weak-memory-model-verifier ❌ |
| webassembly-runtime ❌ | webassembly-verifier ❌ |
Legend: ✅ Verified | 🔶 Partially Verified | ❌ Unverified
To help verify a skill, see Contributing Guidelines.
Browse, search, and install skills through our interactive web interface.
This repository contains 98 PL research skills designed for:
- PL researchers - Type systems, formal semantics, proof assistants
- Compiler practitioners - Compiler passes, program analysis, optimizations
- Systems engineers - Runtime systems, verification, concurrency
- Graduate students - Learning PL concepts through working implementations
- Tool builders - Building compilers, analyzers, and verifiers
Each skill is a self-contained implementation that can solve real PL research problems:
- Task-grounded (solves concrete PL problems)
- Reusable (clearly specified inputs/outputs)
- Tool-aware (operates on real code, specifications, proofs)
| Skill | Description |
|---|---|
| type-checker-generator | Generates type checkers from language specifications |
| type-inference-engine | Implements Hindley-Milner type inference |
| subtyping-verifier | Verifies subtyping relations |
| simply-typed-lambda-calculus | STLC with products, sums, booleans |
| dependent-type-implementer | Dependent types (Pi, Sigma, equality) |
| linear-type-implementer | Linear lambda calculus with resources |
| session-type-checker | Session types for communication protocols |
| ownership-type-system | Ownership and borrowing (like Rust) |
| effect-type-system | Effect tracking for side effects |
| refinement-type-checker | Refinement types with predicates |
| relational-parametricity-prover | Proves parametricity theorems |
| bidirectional-type-checking | Bidirectional type inference/checking |
| row-polymorphism | Extensible records with row types |
| polymorphic-effects | Effect polymorphism and handlers |
| higher-order-abstract-syntax | HOAS for binder representation |
| type-directed-name-resolution | Type-guided name disambiguation |
| system-f | System F polymorphic lambda calculus |
| gadt-implementer | Generalized algebraic data types |
| gradual-typing-implementer | Gradual typing system |
| type-class-implementer | Type class implementation |
| existential-types | Existential type implementation |
| Skill | Description |
|---|---|
| operational-semantics-definer | Defines SOS semantics for languages |
| denotational-semantics-builder | Builds denotational semantics |
| axiomatic-semantics | Axiomatic semantics for programs |
| reduction-semantics | Reduction semantics for evaluation |
| hoare-logic-verifier | Verifies programs with Hoare logic |
| separation-logician | Separation logic for heap verification |
| coq-proof-assistant | Proofs in Coq (induction, tactics) |
| bisimulation-checker | Proves bisimilarity between programs |
| contextual-equivalence | Contextual equivalence proofs |
| Skill | Description |
|---|---|
| lambda-calculus-interpreter | Untyped and simply-typed lambda calculus |
| closure-converter | Transforms closures to environment passing |
| lexer-generator | Generates lexical analyzers |
| parser-generator | Generates LALR/recursive descent parsers |
| ssa-constructor | Builds Static Single Assignment form |
| jit-compiler-builder | JIT compilation infrastructure |
| typed-assembly-language | Typed assembly language verifier |
| cps-transformer | Continuation-passing style transform |
| partial-evaluator | Program specialization via PE |
| defunctionalization | Closure elimination to data types |
| multi-stage-programming | Staged compilation and code gen |
| dsl-embedding | Embedding DSLs in host languages |
| Skill | Description |
|---|---|
| dataflow-analysis-framework | General dataflow analysis framework |
| abstract-interpretation-engine | Abstract interpretation engine |
| alias-and-points-to-analysis | Points-to and alias analysis |
| taint-analysis | Taint tracking for security |
| model-checker | Finite-state model checking |
| control-flow-analysis | Control flow analysis |
| escape-analysis | Escape analysis for allocation optimization |
| information-flow-analyzer | Information flow security analysis |
| interprocedural-analysis | Interprocedural program analysis |
| liveness-analysis | Liveness analysis for registers |
| shape-analysis | Shape analysis for heap structures |
| value-analysis | Value range analysis |
| Skill | Description |
|---|---|
| garbage-collector-implementer | GC (mark-compact, generational) |
| constant-propagation-pass | Dataflow constant propagation |
| common-subexpression-eliminator | CSE optimization pass |
| incremental-computation | Change propagation and adaptivity |
| dead-code-eliminator | Dead code elimination pass |
| inline-expander | Function inlining optimization |
| loop-optimizer | Loop optimizations (unrolling, fusion) |
| register-allocator | Graph coloring register allocation |
| memory-allocator | Memory allocation strategies |
| program-transformer | General program transformations |
| Skill | Description |
|---|---|
| acsl-annotation-assistant | ACSL annotations for C/C++ formal verification |
| symbolic-execution-engine | Symbolic execution engine |
| loop-termination-prover | Proves loop termination |
| weak-memory-model-verifier | Verifies weak memory behaviors |
| dafny-verifier | Dafny verification language |
| concurrency-verifier | Concurrency correctness verification |
| lean-prover | Lean theorem prover |
| webassembly-verifier | WebAssembly module verification |
| rust-borrow-checker | Rust borrow checker implementation |
| Skill | Description |
|---|---|
| actor-model-implementer | Actor concurrency model |
| software-transactional-memory | STM implementation |
| race-detection-tool | Dynamic race detection |
| lock-free-data-structure | Lock-free concurrent data structures |
| message-passing-system | Message passing concurrency |
| transactional-memory | Transactional memory implementation |
| capability-system | Capability-based security |
| Skill | Description |
|---|---|
| fuzzer-generator | Fuzzing test generation |
| property-based-tester | Property-based testing |
| sandbox-builder | Sandbox isolation for safe execution |
| Skill | Description |
|---|---|
| smt-solver-interface | Interface to SMT solvers |
| invariant-generator | Infers loop invariants |
| Skill | Description |
|---|---|
| algebraic-effects | Algebraic effects and handlers |
| effect-handlers-implementer | Effect handler implementation |
| effect-system | Effect system for side effects |
| monad-transformer | Monad transformer stacks |
| Skill | Description |
|---|---|
| webassembly-runtime | WebAssembly runtime implementation |
| graalvm-truffle-implementer | GraalVM Truffle language implementation |
| abstract-machine | Abstract machine for semantics |
| Skill | Description |
|---|---|
| ffi-designer | Foreign function interface design |
| language-server-protocol | LSP implementation |
| module-system | Module system design |
| macro-expander | Macro expansion system |
| llvm-backend-generator | LLVM backend generation |
| mlir-dialect-designer | MLIR dialect design |
Each skill is packaged as a folder containing a SKILL.md file.
# Copy the skill folder to your skills directory
cp -r skill-folder ~/.claude/skillsSkills are automatically triggered based on user requests matching the skill description. You can also explicitly invoke a skill:
Using "type-checker-generator" to generate a type checker for my language
We welcome contributions from:
- PL researchers (new skills for type systems, semantics, verification)
- Compiler developers (optimization passes, analysis frameworks)
- Formal methods practitioners (proof assistants, model checkers)
Please read Contributing Guidelines before submitting.
Skills inspired by:
End-to-end workflows composed from multiple skills:
| Pipeline | Description |
|---|---|
| compiler-pipeline | Build a compiler from source to native code |
| verification-pipeline | Verify program correctness |
| type-system-pipeline | Implement a complete type system |
See pipelines/ for more details.