Chris Henson - Locally Nameless Lambda Calculi (Lean Together 2026)
Автор: leanprover community
Загружено: 2026-01-28
Просмотров: 302
Описание:
This talk will discuss CSLib's locally nameless formalization of lambda calculi, which currently includes STLC and System F with subtyping. While this is a well-established style of formalization, we use Lean's new proof automation features and metaprogramming in ways that are interesting to consider. We make heavy use of the grind tactic, allowing us to easily reuse existing Mathlib infrastructure for typing contexts and in general enable a succinct style that is approximately 45% fewer LoC than comparable formalizations. Metaprogramming has also been useful, allowing us to standardize certain notations and develop a single term elaborator for selecting fresh variables that does not require specialization for each type system.
---
Conference website: https://leanprover-community.github.i...
Full schedule: https://leanprover-community.github.i...
Lean community: https://leanprover-community.github.io/
Повторяем попытку...
Доступные форматы для скачивания:
Скачать видео
-
Информация по загрузке:
