OpenSkillIndex← back to search
claude-codescience

Babysitter soundness-proof-assistant

Assist in constructing type soundness proofs using progress and preservation theorems

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/soundness-proof-assistant" ~/.claude/skills/a5c-ai-babysitter-soundness-proof-assistant && rm -rf "$T"
manifest: library/specializations/domains/science/computer-science/skills/soundness-proof-assistant/SKILL.md
tags
#type-theory#proof-assist#theorem-proving#programming-language-theory#formal-verification
source content

Soundness Proof Assistant

Purpose

Provides expert guidance on constructing type soundness proofs for programming language type systems.

Capabilities

  • Progress theorem proof templates
  • Preservation theorem proof templates
  • Substitution lemma generation
  • Canonical forms lemma derivation
  • Proof case enumeration
  • Mechanization guidance

Usage Guidelines

  1. Lemma Identification: Identify required supporting lemmas
  2. Progress Proof: Prove progress theorem by cases
  3. Preservation Proof: Prove preservation theorem
  4. Substitution Lemmas: Prove substitution preserves typing
  5. Mechanization: Translate to proof assistant

Tools/Libraries

  • Coq
  • Agda
  • Lean
  • Twelf