HORIP SIGNED
Higher-Order Rewriting for Intensional Properties of Programs and Circuits
Total Cost €
0EC-Contrib. €
0Partnership
0Views
0HORIP project word cloud
Explore the words cloud of the HORIP project. It provides you a very rough idea of what is the project "HORIP" about.
Project "HORIP" data sheet
The following table provides information about the project.
| Coordinator |
KOBENHAVNS UNIVERSITET
Organization address contact info |
| Coordinator Country | Denmark [DK] |
| Project website | https://www.cs.ru.nl/ |
| Total cost | 200˙194 € |
| EC max contribution | 200˙194 € (100%) |
| Programme |
1. H2020-EU.1.3.2. (Nurturing excellence by means of cross-border and cross-sector mobility) |
| Code Call | H2020-MSCA-IF-2014 |
| Funding Scheme | MSCA-IF-EF-ST |
| Starting year | 2015 |
| Duration (year-month-day) | from 2015-10-01 to 2017-09-30 |
Partnership
Take a look of project's partnership.
| # | ||||
|---|---|---|---|---|
| 1 | KOBENHAVNS UNIVERSITET | DK (KOBENHAVN) | coordinator | 200˙194.00 |
Map
Project objective
'The HORIP project will employ higher-order term rewriting to characterise intensional program properties: properties concerned with 'how' rather than 'what' a program computes, such as complexity, compressibility and safety.
Term rewriting is a formal system which can be used to specify algorithms. Unlike common programming languages, term rewriting has a simple, formal definition which admits non-determinism. Higher-order term rewriting is an extension therof, which shares these advantages but has greater expressivity.
To analyse program properties, we may either use dedicated techniques, or translate queries into different fields, with term rewriting as a powerful option. In doing so, methods from widely different areas can be applied.
HORIP aims to analyse intensional properties using higher-order term rewriting. The first phase will attack two lines of research ripe for success: implicit complexity and compiler correctness. For the former, the supervisor is an expert in complexity and the fellow in higher-order term rewriting. For the latter, we will work together with industry collaborator Dr. Rose, who develops the CRSX framework which seeks to describe compilers using a special form of higher-order term rewriting. Leveraging the expertise of all three parties and potential local collaborators, strong results are expected, especially since the higher-order setting avoids many intrinsic limitations of previous work. In the second phase, we extend these ideas to complexity and compressibility of logical circuits. This builds on the first year's experience with implicit complexity, and the expertise of the scientist-in-charge.
HORIP is basic research, building on very recent advances from several international research groups. There are potential future business applications, as well as also purely theoretical goals. All results and related code will be published open source, so as to aid both basic and applied followup research. '
Publications
| year | authors and title | journal | last update |
|---|---|---|---|
| 2016 |
Cynthia Kop, Jakob Grue Simonsen Higher-order Cons-free Interpreters published pages: , ISSN: , DOI: |
Higher Order Rewriting: HOR 2016 | 2019-06-14 |
| 2017 |
Cynthia Kop Cons-free Programming with Immutable Functions published pages: , ISSN: , DOI: |
Developments in Implicit Computational complExity: DICE 2017 | 2019-06-14 |
| 2017 |
Cynthia Kop and Aart Middeldorp and Thomas Sternagel Complexity of Conditional Term Rewriting published pages: , ISSN: 1860-5974, DOI: |
Logical Methods in Computer Science (lmcs:3123) 13/1 | 2019-06-14 |
| 2016 |
Cynthia Kop, Kristoffer Rose h: A Plank for Higher-order Attribute Contraction Schemes published pages: , ISSN: , DOI: |
Higher Order Rewriting: HOR 2016 | 2019-06-14 |
| 2016 |
Cynthia Kop Non-deterministic Characterisations published pages: , ISSN: , DOI: |
Workshop on Termination: WST 2016 | 2019-06-14 |
| 2017 |
Cynthia Kop and Jakob Grue Simonsen Complexity Hierarchies and Higher-order Cons-free Term Rewriting published pages: , ISSN: 1860-5974, DOI: |
Logical Methods in Computer Science (lmcs:3847; Special Issue for FSCD 2016) 13/3 | 2019-06-14 |
| 2017 |
Carsten Fuhs, Cynthia Kop, Naoki Nishida Verifying Procedural Programs via Constrained Rewriting Induction published pages: 1-50, ISSN: 1529-3785, DOI: 10.1145/3060143 |
ACM Transactions on Computational Logic 18/2 | 2019-06-14 |
| 2016 |
Cynthia Kop On First-order Cons-free Term Rewriting and PTIME published pages: , ISSN: , DOI: |
Developments in Implicit Computational complExity: DICE 2016 | 2019-06-14 |
Are you the coordinator (or a participant) of this project? Plaese send me more information about the "HORIP" project.
For instance: the website url (it has not provided by EU-opendata yet), the logo, a more detailed description of the project (in plain text as a rtf file or a word file), some pictures (as picture files, not embedded into any word file), twitter account, linkedin page, etc.
Send me an email (fabio@fabiodisconzi.com) and I put them in your project's page as son as possible.
Thanks. And then put a link of this page into your project's website.
The information about "HORIP" are provided by the European Opendata Portal: CORDIS opendata.