TinkerType: a language for playing with formal systems
TinkerType: a language for playing with formal systems
复制标题
TinkerType：一种用于玩弄正式系统的语言
DOI：
--
复制
发表时间：
2003
影响因子：
1.1
通讯作者：
B. Pierce
中科院分区：
文献类型：
--
作者：
Michael Y. Levin;B. Pierce
TinkerType是一种用于形式系统(类型系统、操作语义、逻辑等)的紧凑和模块化描述的实用框架。一系列相关系统被分解为一组子句--单个推理规则--和一组控制特定系统中包含子句的特征。简单的静态检查用于帮助维护生成的系统的一致性。我们介绍了TinkerType及其实现，并描述了它在两个重要的类型化lambda演算存储库中的应用。第一个存储库涵盖了广泛的类型功能，包括子类型、多态、类型操作符和绑定、计算效果和依赖类型。它描述了系统的声明性和算法方面，可以与我们的工具TinkerType汇编程序一起使用，以推理规则的排版集合的形式或作为可执行的ML类型检查器生成演算。第二个存储库针对较小的系统集合，并提供基本安全属性的模块化证明。
TinkerType is a pragmatic framework for compact and modular description of formal systems (type systems, operational semantics, logics, etc.). A family of related systems is broken down into a set of clauses – individual inference rules – and a set of features controlling the inclusion of clauses in particular systems. Simple static checks are used to help maintain consistency of the generated systems. We present TinkerType and its implementation and describe its application to two substantial repositories of typed lambda-calculi. The first repository covers a broad range of typing features, including subtyping, polymorphism, type operators and kinding, computational effects, and dependent types. It describes both declarative and algorithmic aspects of the systems, and can be used with our tool, the TinkerType Assembler, to generate calculi either in the form of typeset collections of inference rules or as executable ML typecheckers. The second repository addresses a smaller collection of systems, and provides modularized proofs of basic safety properties.