BrainMap

Mircea-Dan Hernest

Researcher - INSTITUTUL ROMAN DE STIINTA SI TEHNOLOGIE

Researcher | Scientific reviewer | Consultant

Web of Science ResearcherID: C-4611-2011

Expertise & keywords

Optimized program synthesis from proofs Call name: Projects for Young Research Teams - TE-2011 call
PN-II-RU-TE-2011-3-0122 2011 - 2014

Role in this project:

Coordinating institution: Institutul de matematica "Simion Stoilow" al Academiei Romane

Project partners: Institutul de matematica "Simion Stoilow" al Academiei Romane (RO)

Affiliation: Institutul de matematica "Simion Stoilow" al Academiei Romane (RO)

Project website: http://sites.google.com/site/te201130122/

Abstract:

Light functional interpretations were introduced by Hernest in his PhD thesis as optimizations of Goedel´s Dialectica interpretation and its monotone variant due to Kohlenbach by adaptation of the uniform quantifiers due to Berger (in a Modified Realizability setting) to the Dialectica context. This was continued with Trifonov by refining the detection of the uniform parts of a quantifier, which implied the addition of new semi-uniform quantifiers. The latest device for more efficient program extraction from proofs is the modal operator, which discards the request for negative computational content from its whole quantified formula. Illustrative applications were presented for all the light tools. We wish to find not only new, but also more complex applications of these light techniques. We target two large classes of applications. The first is new algorithms for various combinatorial problems for which at most certain heuristic approaches yield somewhat better results than the blunt search in the solutions space. The second is related to the Proof Mining project of Kohlenbach: in his 2008 book he outlines four ambitious research directions for the construction of new quantitative (sometimes qualitative) data out of existing recent celebrated proofs in Mathematics. We also want to compare the output of the light modal Dialectica interpretation with that of Escardo and Oliva's Pierce translation on certain classical proofs of mathematical theorems in the proof-assistat MinLog

FILE DESCRIPTION	DOCUMENT
List of research grants as project coordinator or partner team leader
Significant R&D projects for enterprises, as project manager
R&D activities in enterprises
Peer-review activity for international programs/projects