课题基金 / 基金详情

CIF: Small: Rich Type Inference for Functional Programming

CIF: Small: Rich Type Inference for Functional Programming
CIF:小型:函数式编程的丰富类型推理
批准号:
1319880
负责人:
Stephanie Weirich
金额:
$45.0万
依托单位:
依托单位国家:
美国
项目类别:
Standard Grant
财政年份:
2013
资助国家:
美国
项目状态:
已结题
起止时间:
2013-09-01 至 2018-08-31

项目摘要

项目成果

Stephanie Weirich的其他基金

相似基金

相关文献

中文摘要
翻译
计算机软件的正确性通常依赖于其在执行过程中对特定于应用的不变量的遵守。这些不变量是复杂的,通常涉及系统的许多不同部分之间的关系,并且是隐式的,通常从未在程序的文本中正式表达。然而,违反这些不变量会导致许多错误和安全漏洞。因此,程序员使用静态类型系统来捕获这些不变量,并允许使用自动化工具来检查它们是否得到维护。 类型推断的算法允许复杂类型保持隐式,从而简化软件开发和维护,同时仍然可以随时用于文档编制和实施。虽然最近的类型系统扩展极大地丰富了静态类型语言的表达能力,但类型推理算法却没有跟上。本研究评估SMT(可满足性模理论)求解器到工业强度的函数式编程语言的类型推理算法的集成。特别是,与微软研究院剑桥的研究人员合作,它扩展了格拉斯哥Haskell算法(GHC)的类型推理算法。 GHC是一个成熟的、开源的Haskell编译器,由于其丰富的类型系统而在工业界越来越受欢迎。该项目还包括教育和推广部分,其形式是高级本科/硕士课程,并得到博士生的直接支持。学生
英文摘要
The correctness of computer software often relies on its adherence to application-specific invariants during the course of its execution. These invariants are complex, often involving relationships between many different parts of the system, and implicit, often never formally expressed in the text of the program. Violating these invariants, however, leads to numerous bugs and security holes. As a result, programmers employ static type systems to capture these invariants and enable the use of automated tools to check that they are maintained. Algorithms for type inference allow complex types to remain implicit, easing software development and maintenance, while still readily available for documentation and enforcement. While recent type system extensions greatly enrich the expressiveness of statically typed languages, type inference algorithms have not kept pace. This research evaluates the integration of SMT (Satisfiability Modulo Theory) solvers into the type inference algorithm of an industrial-strength functional programming language. In particular, in collaboration with researchers at Microsoft Research Cambridge, it extends the type inference algorithm of the Glasgow Haskell Compiler (GHC). GHC is a mature, open source, Haskell Compiler that is gaining popularity in industry due to its rich type system. The project also includes education and outreach components in the form of an advanced undergraduate/masters level course and in the direct support of Ph.D. students.
期刊论文(5)
专著(0)
科研奖励(0)
会议论文
DOI: 10.1145/3167092
发表时间: 2017-11
期刊: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
影响因子: --
作者: [Antal Spector-Zabusky;Joachim Breitner;C. Rizkallah;Stephanie Weirich]
通讯作者: Antal Spector-Zabusky;Joachim Breitner;C. Rizkallah;Stephanie Weirich
Keep your laziness in check
控制你的懒惰
DOI: 10.1145/3236797
发表时间: 2018
期刊: Proceedings of the ACM on Programming Languages
影响因子: --
作者: [Foner, Kenneth, Zhang, Hengchu, Lampropoulos, Leonidas]
通讯作者: Lampropoulos, Leonidas
A specification for dependent types in Haskell
Haskell 中依赖类型的规范
DOI: 10.1145/3110275
发表时间: 2017
期刊: Proceedings of the ACM on Programming Languages
影响因子: --
作者: [Weirich, Stephanie, Voizard, Antoine, de Amorim, Pedro Henrique, Eisenberg, Richard A.]
通讯作者: Eisenberg, Richard A.
A role for dependent types in Haskell
Haskell 中依赖类型的角色
DOI: 10.1145/3341705
发表时间: 2019
期刊: Proceedings of the ACM on Programming Languages
影响因子: --
作者: [Weirich, Stephanie, Choudhury, Pritam, Voizard, Antoine, Eisenberg, Richard A.]
通讯作者: Eisenberg, Richard A.
SHF: SMALL:Dependency Tracking and Dependent Types
  • 批准号:
    2327738
  • 项目类别:
    Standard Grant
  • 资助金额:
    $54.0万
  • 财政年份:
    2023
  • 负责人:
    Stephanie Weirich
  • 依托单位:
SHF: Small: Mechanized reasoning for functional programs
  • 批准号:
    2006535
  • 项目类别:
    Standard Grant
  • 资助金额:
    $45.0万
  • 财政年份:
    2020
  • 负责人:
    Stephanie Weirich
  • 依托单位:
SHF: Medium: Collaborative Research: The Theory and Practice of Dependent Types in Haskell
  • 批准号:
    1703835
  • 项目类别:
    Continuing Grant
  • 资助金额:
    $63.87万
  • 财政年份:
    2017
  • 负责人:
    Stephanie Weirich
  • 依托单位:
STUDENT MENTORING WORKSHOP AT ICFP 2015
  • 批准号:
    1541646
  • 项目类别:
    Standard Grant
  • 资助金额:
    $2.03万
  • 财政年份:
    2015
  • 负责人:
    Stephanie Weirich
  • 依托单位:
国内基金
海外基金
昼夜节律性small RNA在血斑形成时间推断中的法医学应用研究
  • 批准号:
  • 项目类别:
    省市级项目
  • 资助金额:
    --
  • 批准年份:
    2024
  • 负责人:
  • 依托单位:
tRNA-derived small RNA上调YBX1/CCL5通路参与硼替佐米诱导慢性疼痛的机制研究
  • 批准号:
  • 项目类别:
    省市级项目
  • 资助金额:
    10.0万元
  • 批准年份:
    2022
  • 负责人:
    张祥忠
  • 依托单位:
Small RNA调控I-F型CRISPR-Cas适应性免疫性的应答及分子机制
Small RNAs调控解淀粉芽胞杆菌FZB42生防功能的机制研究
  • 批准号:
    31972324
  • 项目类别:
    面上项目
  • 资助金额:
    58.0万元
  • 批准年份:
    2019
  • 负责人:
    高学文
  • 依托单位: