Hola,
¿eres nuevo aquí?

Regístrate gratis y conecta tu empresa con financiación pública, partners y proyectos.

Tengo cuenta

Regístrate

Ver video

TypeSynth

Financiado

Synthetic Methods in Program Verification

TypeSynth: Synthetic Methods in Program Verification Software systems mediate a growing proportion of human activity, e.g. communication, transport, medicine, industrial and agricultural production, etc. As a result, it is urgent... ver más

30/06/2024

215K€

Presupuesto del proyecto: 215K€

Líder del proyecto

AARHUS UNIVERSITET No se ha especificado una descripción o un objeto social para esta compañía.

TRL 4-5

Fecha límite participación Sin fecha límite de participación.

Financiación concedida El organismo HORIZON EUROPE notifico la concesión del proyecto el día 2024-06-30

HORIZON-MSCA-2021-PF-01-01: MSCA Postdoctoral Fellowships 2021 ExpectedOutcome:

I+D

Cerrada hace 3 años

0% 100% 100%

Información adicional privada

No hay información privada compartida para este proyecto. Habla con el coordinador.

1 Participantes

214.93K€ | Lider

Conecta tu I+D

¿Tienes un proyecto y buscas un partner? Gracias a nuestro motor inteligente podemos recomendarte los mejores socios y ponerte en contacto con ellos. Te lo explicamos en este video

Proyectos interesantes

CHORDS Compositional Higher-Order Reasoning about Distributed Syste... 2M€ Cerrado

TIN2008-05624 DESARROLLO DE SOFTWARE VERIFICABLE Y EFICIENTE 505K€ Cerrado

TIN2016-81699-ERC ESTRUCTURAS DE TIPO Y PRUEBA PARA VERIFICACION DE SOFTWARE C... 75K€ Cerrado

TIN2010-20639 VERIFICACION PARAMETRIZADA DE SISTEMAS INFORMATICOS 44K€ Cerrado

CRETE Certified Refinement Types 2M€ Cerrado

HYPER Logics and Algorithms for a Unified Theory of Hyperpropertie... 2M€ Cerrado

Duración del proyecto: 24 meses Fecha Inicio: 2022-06-16
Fecha Fin: 2024-06-30

Líder del proyecto

AARHUS UNIVERSITET No se ha especificado una descripción o un objeto social para esta compañía.

TRL 4-5

Presupuesto del proyecto 215K€

Fecha límite de participación Sin fecha límite de participación.

Descripción del proyecto TypeSynth: Synthetic Methods in Program Verification Software systems mediate a growing proportion of human activity, e.g. communication, transport, medicine, industrial and agricultural production, etc. As a result, it is urgent to understand and better control both the correctness and security properties of these increasingly complex software systems. The diversity of verification requirements speaks to a need for models of program execution that smoothly interpolate between many different levels of abstraction. Models of program execution vary in expressiveness along the spectrum of possible programming languages and specification logics. At one extreme, dependent type theory is a language for mathematically-inspired functional programming that is sufficiently expressive to serve as its own specification logic. Dependent type theory has struggled, however, to incorporate several computational effects that are common in every-day programming languages, such as state and concurrency. Languages that support these features require very sophisticated specification logics due to the myriad details that must be surfaced in their semantic models. In the context of dependent type theory, I have recently developed a new technique called Synthetic Tait Computability or STC that smoothly combines multiple levels of abstraction into a single language. Inspired by sophisticated mathematical techniques invented in topos theory and category theory for entirely different purposes, STC enables low-level details (even down to execution steps) to be manipulated in a simpler and more abstract way than ever before, making them easier to control mathematically. Perhaps more importantly, the STC method makes it possible to import ideas and techniques from other fields that seemed more distant prior to my intervention. The goal of the TypeSynth project is to extend the successful STC approach to a wider class of programming models, in particular programming languages with effects.

Conecta tu I+D

Entra hoy

¿Olvidé mi contraseña?

Financiación

Empresas

CTIs/Universidades

Proyectos

Investigadores