Optimized program synthesis from proofs / Sinteza de programe optimizate din demonstratzii [ project report ] - financed through UEFISCDI by the Romanian Ministry of Education human resources - young teams - 2011 competition [ list ] contract 24 / 2011-10-05 - - the main objective of this project has been the design and implementation of the (light) modal functional interpretation, which we have successfully fulfilled - SchuetteModal IMAR Location dexonline.ro dict.org lexilogos.com leo.org implemented Kreisel implication 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-assistant MinLog. Articol Wikipedia despre Interpretarea Functzionala a lui Goedel PhD Comics Dilbert Comics FBprojectSpeaker Descrierea limbajului de programare Scheme Ghid Utilizator al Limbajului de programare functzionala Scheme http://minlog-system.de http://coq.inria.fr MinLogForDialectica Homepage Dan Hernest Bucharest Seminar on Logic in Computer Science Bucharest ILogic Seminar LambdaNotes is the simplest possible programming language that is Turing complete. Because of its simplicity, it is a useful tool fordefining and proving properties of programs. Many real-world programming languages can be regardedas extensions of the lambda calculus.This is true for all Functional_programming languages,http://en.wikipedia.org/wiki/Functional_programming a class that includes Lisp, Scheme, Haskell, and ML. Such languages combine the lambda calculus with additional features,such as data types, input/output, side effects, udpateable memory,object orientated features, etc.Thelambda calculus provides a vehicle for studying such extensions, in isolation and jointly , to see ho w the y will af fect each other , and to prove properties of programming languages (such as: a well-formed program will not crash). |