Agent Skills: Typing Rule Generator

Generate and format typing rules in inference rule notation for type system design

programming-language-theoryID: a5c-ai/babysitter/typing-rule-generator

Install this agent skill to your local

pnpm dlx add-skill https://github.com/a5c-ai/babysitter/tree/HEAD/plugins/babysitter/skills/babysit/process/specializations/domains/science/computer-science/skills/typing-rule-generator

Skill Files

Browse the full folder contents for typing-rule-generator.

Download Skill

Loading file tree…

plugins/babysitter/skills/babysit/process/specializations/domains/science/computer-science/skills/typing-rule-generator/SKILL.md

Skill Metadata

Name
typing-rule-generator
Description
Generate and format typing rules in inference rule notation for type system design

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