O intâlnire cu informatica teoretică românească: FMI@150 Ziua I

Sfârșitul acesta de săptămână voi fi la București, spre care mă indrept in momentul in care scriu rândurile acestea (joi seara, in trenul Timișoara-București): Facultatea de Matematicâ și Informatică a Universității din București, cea pe care cu onor am absolvit-o acum …. mulți, mulți ani aniversează 150 de ani de la inființare. In cinstea acestui moment a fost organizată o conferință științifică aniversară. Nu am putut ajunge la deschidere. Așa că nu vă pot povesti despre prezentarea profesorului Solomon Marcus. Cunoscându-l de atâta amar de vreme n-am nicio indoială că a fost una deosebită, insă promit să mă revanșez.

Conferința științifică efectivă  incepe abia in ziua (vineri) in care mesajul acesta va apărea pe blog. Mi-am propus să fac un lucru pe care nu l-am mai văzut in blogosfera românească: live blogging de la un eveniment științific.

Fatalmente voi fi obligat să aleg din multele secțiuni ale al conferinței. Voi merge la secțiunea de care sunt legat din punct de vedere științific, cea de informatică (teoretică).

Mesajul acesta va fi continuu actualizat in cursul zilei de azi. Stay tuned !

Programul de azi:

Cristian Calude (Auckland)- Anytime algorithms with algorithmic incompressibility cutoffs.

criscaludeCris este unul dintre oamenii responsabili pentru inceputurile mele științifice și mă bucur de fiecare dată  să-l reintâlnesc. Prezentarea sa a aplicat unele idei venind dinspre zona teoriei algoritmice a informației in domeniul algoritmilor anytime. Un algoritm anytime este unul pentru care produce in mod continuu soluții pentru o instanță a unei probleme, calitatea soluțiilor imbunătățindu-se in continuu. Aplicația a vizat studiul așa numiților timpi de cutoff, momente in care intrerupem un algoritm anytime. Cum spuneam, rezultatele de teoria algoritmică a informației, in mod specific conceptul de incompresibilitate (algoritmică) pot specifica timpii de cutoff.

Dincolo de prezentarea propriu zisă, câteva fraze din prezentare:

„o teorie matematică imbină două componente: componenta de modelare și componenta metaforică. „

„Arbitrul final, cel care ne lasa sa programăm, este fizica. „

Cătălin Dima (Paris Est-Creteil) – The epistemic \mu-calculus.

catalindima

Cătălin mi-a fost coleg de generație … mai pe urmă interesele noastre de cercetare au evoluat in direcții foarte diferite. In prezentarea de la FMI-150, Cătălin a oferit, pe lângă o introduce in probleme legate de logici temporale și legătura cu probleme de tip model checking,  definiția unei logici de tip \mu-calcul pe arbori care combină aspectele temporale cu cele epistemice. Noul formalism conduce la unele probleme logice interesante privind legătura cu logica monadică de ordinul doi pe arbori.

 

Bogdan Warinschi (Bristol) – Computational soundness in security protocol analysis.

bogdanwarinschiCu Bogdan nu mă cunoșteam personal, deși am studiat amândoi in Statele Unite și avem prieteni buni (Luță – Grigore Roșu pe numele oficial). Bogdan e cercetător in domeniul criptografiei și ne-a prezentat cele două paradigme ale teoriei moderne a acestui domeniu: paradigma computațională (bazate pe modele de tip mașini Turing, distribuții de probabilitate, etc) și cea simbolică, bazate pe logică demonstrații automate. Dacă prima paradigmă este mai puternică/expresivă, cea de-a doua oferă cadrul preferat de criptografi, fiind mai sistematică.

Bogdan s-a referit (drept un caz concret) la formalizarea in cele două paradigme a noțiunii de secrecy. Așa numite soundness theorem conectează, cum a arătat Bogdan, cele două formalizări.

Viorica Sofronie-Stokkermans (Max Planck-Saarbrucken)- Hierarchical reasoning in local theory extensions and applications.

SAMSUNG

Pe Viorica am cunoscut-o abia la această intâlnire. Pe de altă parte prezentarea ei mi-a fost intr-un anumit sens una din cele mai familiare de până acum. Lucru de ințeles, având in vedere faptul câ Viorica și-a făcut studiile doctorale la RISC in Hagenberg (Linz) Austria, ca și legăturile evidente dintre Universitatea de Vest din Timișoare și acest institut.

Viorica a vorbit despre logici care combină exemple de teorii complexe, dar in care raționamentele pot fi deseori făcute eficient in mod ierarhic, exploatând poate diferite aspecte ale acestor teorii in părți diferite ale demonstrației. Acest lucru nu este posibil intotdeauna. O proprietate care asigură efectivitatea acestui proces ține de o anumită natură locală a formulelor implicate.

Cum am spus, o prezentare interesantă pe o temă care nu imi e complet necunoscută. Poate aș fi dorit să fi aflat mai mult despre aspectele ținând de complexitatea algoritmilor la care se face aluzie in rezumat. Pe de altă parte, recunosc, interesul meu in această direcție nu este impărtășit, cred, de ceilalți participanți.

Laurențiu Leuștean (IMAR/UB)- Proof mining and applications in nonlinear ergodic theory.

SAMSUNGLaurențiu e coleg de Ad-Astra și absolvent al aceleeași facultăți. Ne-a vorbit despre proof mining, o tehnică de a extrage conținutul „constructiv” dintr-o demonstrație matematică. Aplicațiile pe care le-a prezentat vin dintr-un domeniu despre care mărturisesc că nu știam mare lucru, prin urmare nu vă pot povesti mai multe.

Pe de altă parte, de faptul că  domeniul este unul interesant vă puteți convinge de exemplu citind această discuție pe blogul lui Terry Tao. Ar fi interesant de văzut câte din lucrurile din acest domeniu pot fi automatizate. Impresia pe care mi-a lăsat-o prezentarea lui Laurențiu e că dificultățile apar la codificarea inițială a faptelor matematice, mai curând decăt in aplicarea metodelor de mining.

Grigore Roșu (Illinois Urbana-Champaign)- Specify and verify your language using K.

SAMSUNGTrebuia să se intâmple 🙂 Prima conferință la care asist la o  prezentare prin Skype (trebuie să spun că voi revedea pe viu prezentarea, in engleză  peste vreo trei săptămâni la Timișoara.

Luță (cum il cunosc prietenii) este unul din cei mai de succes informaticieni români. După un doctorat la UC San Diego și un stagiu in cercetare la NASA Ames, Luță este profesor asociat la Urbana și un cercetâtor de succes in domeniul runtime verification și alte metode formale. Aici a ales să vorbească de „copilul său” din domeniul limbajelor de programare, așa-numitul sistem K. Ce este K ? Conform prezentării la care tocmai asist 🙂 este un framework care iși propune să ușureze definirea limbajelor de programare, nu doar la nivel sintactic (lucru in esență deja făcut) cât și, mult mai greu, la nivel semantic. K are un model vizual atractiv, iar semantica poate fi explicată cel mai bine cu  graph rewriting. K permite „definirea” multor limbaje reale (VERILOG, Java, Python, C). …

The most complete formal C semantics [POPL 2012] … Și o prezentare de nivel de vârf din informatica teoretică „de tip B” (nu e o judecată de valoare ci o impărțire a subdomeniilor informaticii teoretice după volumele din Handbook of Theoretical Computer Science)

Seara a mai conținut o continuare informală pe terasă la Casa Armatei 🙂 Din păcate telefonul meu descărcat nu mi-a mai permis sa fac poze și acolo.

In concluzie: o zi lungă, cu prezentări extinse: durata alocată fiecărui vorbitor era de o oră, lucru care, recunosc, mi-a plăcut. Ziua a avut o anume unitate stilistică, cu excepția prezentării lui Cris Calude celelalte ținând de zona logicii și metodelor formale. Cer scuze pentru calitatea slabă a unora din poze, au fost făcute cu telefonul mobil, in condiții de iluminare nu dintre cele mai bune.

Pe mâine.

Anunțuri
Acest articol a fost publicat în evenimente, informaticã teoreticã. Pune un semn de carte cu legătura permanentă.

Lasă un răspuns

Completează mai jos detaliile tale sau dă clic pe un icon pentru a te autentifica:

Logo WordPress.com

Comentezi folosind contul tău WordPress.com. Dezautentificare / Schimbă )

Poză Twitter

Comentezi folosind contul tău Twitter. Dezautentificare / Schimbă )

Fotografie Facebook

Comentezi folosind contul tău Facebook. Dezautentificare / Schimbă )

Fotografie Google+

Comentezi folosind contul tău Google+. Dezautentificare / Schimbă )

Conectare la %s