---
name: typing-rule-generator
description: Generate and format typing rules in inference rule notation for type system design
allowed-tools:
  - Bash
  - Read
  - Write
  - Edit
  - Glob
  - Grep
metadata:
  specialization: computer-science
  domain: science
  category: programming-language-theory
  phase: 6
---

# Typing Rule Generator

## Purpose

Provides expert guidance on generating typing rules for programming language design using formal inference rule notation.

## Capabilities

- LaTeX inference rule generation
- Syntax-directed rule derivation
- Typing derivation tree construction
- Rule dependency analysis
- Export to Ott/LNGen format
- Handle subtyping and polymorphism

## Usage Guidelines

1. **Syntax Definition**: Define language syntax formally
2. **Rule Design**: Design typing rules for each construct
3. **Derivation Trees**: Build typing derivation examples
4. **Formatting**: Generate publication-quality rules
5. **Export**: Export to mechanization tools

## Tools/Libraries

- LaTeX (mathpartir)
- Ott
- LNGen
- PLT Redex