| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | August 24, 2009 |
| Latest Amendment Date: | August 24, 2009 |
| Award Number: | 0910500 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Sol Greenspan
sgreensp@nsf.gov (703)292-7841 CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | September 1, 2009 |
| End Date: | August 31, 2014 (Estimated) |
| Total Intended Award Amount: | $668,182.00 |
| Total Awarded Amount to Date: | $668,182.00 |
| Funds Obligated to Date: |
|
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
1600 SW 4TH AVE PORTLAND OR US 97201-5508 (503)725-9900 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
1600 SW 4TH AVE PORTLAND OR US 97201-5508 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): |
Information Technology Researc, PROGRAMMING LANGUAGES |
| Primary Program Source: |
|
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
The cost-effective construction of functionally correct software systems remains an unmet challenge for Computer Science. Although industrial best practices for software construction (such as testing, code reviews, automatic bug finding) have low cost, they cannot provide strong guarantees about correctness. Classical verification methods, on the other hand, are not cost-effective. Recently, the research community has been exploring the idea of dependent types, which extend the expressive power of programming languages to support verification. These rich types allow the programmer to express non-trivial invariant properties of her data and code as a part of her program. That way, verification is incremental, localized and at source-language level.
This multi-institution collaborative project is for the design and implementation of a programming language with dependent types, called Trellys. Technically, Trellys is call-by-value functional programming language with full-spectrum dependency. Overall, the project combines numerous fragmented research results into a coherent language design, by building a robust open-source implementation. The design draws on diverse solutions to the technical problems that arise from extending traditional programming languages accommodate dependent types: type and effect inference, language interoperability, compilation, and concurrency.
PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH
Note:
When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external
site maintained by the publisher. Some full text articles may not yet be available without a
charge during the embargo (administrative interval).
Some links on this page may take you to non-federal websites. Their policies may differ from
this site.
Please report errors in award information by writing to: awardsearch@nsf.gov.
