Recherchiere Firmenbekanntmachungen und finanzielle Kennzahlen
UK-Förderung (96.582 £): Haskell-Typen mit Mehrwert Ukri30.06.2012 Forschung und Innovation im Vereinigten Königreich, Großbritannien
Auf einen Blick
Text
Haskell-Typen mit Mehrwert
| Zusammenfassung | Good ideas, like lightning, take the most conductive path to earth. This one-year project takes advantage of fresh technological insights to narrow the spark-gap from theoretical research to the programming mainstream. In the last decade, dependent types --- capturing relative notions of data validity --- have jumped from logics and proof systems to programming. Prototype languages such as Cayenne, ATS, Agda and our own Epigram teach us how to characterize data precisely, but none has a coherent treatment of interaction in applications. This project will bring the basics of dependent types to application development now, not via a prototype, but with Haskell, a mature functional programming language with growing traction, thanks to the Glasgow Haskell Compiler (GHC), now developed under the Microsoft aegis. To make this jump, we must give practical answers to theoretical questions about the mathematical structures which underpin interactive and distributed systems. We must take the blackboard to the motherboard. The tool which enables this project is our GHC preprocessor, the Strathclyde Haskell Enhancement (SHE), which mechanizes a partial translation from 'dependently typed Haskell' to Haskell as it stands. Up and running, SHE has already delivered the basics of our approach, leading to an article accepted in 2011 by the Journal of Functional Programming, and spurring deeper investigation of both the mathematics of dependently typed interaction and the engineering challenge of scaling up. Through theoretical research, library design and case study, we shall deliver progress across this spectrum through papers and open source software. GHC is adopting our functionality, but we do not need to wait. SHE can sustain low-cost exploration, putting an effective toolkit in users' hands now, as well as informing the future prospectuses both for dependent types in Haskell and for programming interaction in the next generation of functional languages. Haskellers recognize the need: Microsoft currently funds a PhD at Strathclyde on numerical dependency in Haskell types. This project is, then, a double fix: it imports dependent types from tomorrow's languages to today's, and it allows us to guide tomorrow's dependently typed languages towards principled approaches to production software. We have proven track records in theoretical research and professional software development, key ideas to change programming for the better, and the skills to deliver world-leading research. |
| Kategorie | Research Grant |
| Referenz | EP/J014591/1 |
| Status | Closed |
| Laufzeit von | 30.06.2012 |
| Laufzeit bis | 29.06.2013 |
| Fördersumme | 96.582,00 £ |
| Quelle | https://gtr.ukri.org/projects?ref=EP%2FJ014591%2F1 |
Beteiligte Organisationen
| University of Strathclyde | |
| Microsoft Research |
Die Bekanntmachung bezieht sich auf einen vergangenen Zeitpunkt, und spiegelt nicht notwendigerweise den heutigen Stand wider. Der aktuelle Stand wird auf folgender Seite wiedergegeben: University of Strathclyde, Glasgow, Großbritannien.
Die Visualisierungen zu "University of Strathclyde - UK-Förderung (96.582 £): Haskell-Typen mit Mehrwert"
werden von
North Data
zur Weiterverwendung unter einer
Creative Commons Lizenz
zur Verfügung gestellt.
