OpenSkillIndex← back to search
claude-codescience

Babysitter typing-rule-generator

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

install
source · Clone the upstream repo
git clone https://github.com/a5c-ai/babysitter
Claude Code · Install into ~/.claude/skills/
T=$(mktemp -d) && git clone --depth=1 https://github.com/a5c-ai/babysitter "$T" && mkdir -p ~/.claude/skills && cp -r "$T/library/specializations/domains/science/computer-science/skills/typing-rule-generator" ~/.claude/skills/a5c-ai-babysitter-typing-rule-generator && rm -rf "$T"
manifest: library/specializations/domains/science/computer-science/skills/typing-rule-generator/SKILL.md
tags
#typing-rules#inference-notation#type-systems#formal-logic#language-design
source content

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