Proiect PN-II-RU-TE-2011-3-0122 ("Young Teams")

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

The  Lambda_calculus   is a very idealized Programming_language; arguably, it        ELIZA
is
the
simplest
possible
programming language
that is Turing complete. Because of its simplicity, it is a useful tool for
defining
and
proving
properties
of
programs.
Many real-world programming languages can be regarded
as 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).