Scholarlink

Dependent types provide users with the tools to embody specifications in types, with implementations carrying proofs that the specifications are met. One approach to developing programs in a dependently typed language develops such programs by enriching simply typed programs through a process of refactoring.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Structural Refactorings for Exploring Dependently Typed Programming

  • 会议论文

  • 发表日期：

    2025年

查看全文
  • Adam D. Barwell,
  • Christopher Brown,
  • Mun See Chang,
  • Constantine Theocharis,
  • Simon Thompson

摘要

Dependent types provide users with the tools to embody specifications in types, with implementations carrying proofs that the specifications are met. One approach to developing programs in a dependently typed language develops such programs by enriching simply typed programs through a process of refactoring.