Projekty finansowane przez NCN
Struktura i interpretacja języków programowania w paradygmacie "dowody jako programy"
2011/03/B/ST6/00348
Słowa kluczowe:
języki programowania izomorfizm Curry'ego-Howarda transformacje programów kontynuacje operatory sterowania interaktywne dowodzenie twierdzeń
Deskryptory:
- ST6_3: Metody formalne
- ST6_7: Teoretyczne podstawy informatyki, w tym informatyka kwantowa
Panel:
ST6 - Informatyka i technologie informacyjne: technologie i systemy informacyjne, informatyka, obliczenia naukowe, systemy inteligentne
Jednostka realizująca:
Uniwersytet Wrocławski, Wydział Matematyki i Informatyki
woj. dolnośląskie
Kierownik projektu (z jednostki realizującej):
Liczba wykonawców projektu: 5
Konkurs: OPUS 2 - ogłoszony 2011-09-15
Przyznana kwota: 399 220 PLN
Rozpoczęcie projektu: 2012-08-31
Zakończenie projektu: 2016-02-29
Planowany czas trwania projektu: 42 miesięcy (z wniosku)
Status projektu: Projekt rozliczony
Zakupiona aparatura
- laptop. Za kwotę 10 000 PLN
- etui na laptopa.
- adapter HDMI-microHDMI, kabel HDMI.
- dysk twardy z etui.
- myszka komputerowa 3 sztuki.
- słuchawki nauszne 2 pary.
- adapter VGA.
Dane z raportu końcowego/rocznego
- Publikacje w czasopismach (1)
- Teksty w publikacjach pokonferencyjnych (7)
- Subtyping Delimited ContinuationsAutorzy:M. Materzok, D. BiernackiCzasopismo:Higher-Order and Symbolic Computation (rok: 2013, tom: nie dotyczy, strony: nie dotyczy), Wydawca: SpringerStatus:Przyjęta do publikacjiDoi:brak - link do publikacji
- A Dynamic Interpretation of the CPS HierarchyAutorzy:M. Materzok, D. BiernackiKonferencja:10th Asian Symposium on Programming Languages and Systems (rok: 2012, ), Wydawca: SpringerData:konferencja December 11-13Status:Opublikowana
- An operational foundation for the tactic language of CoqAutorzy:W. Jedynak, M. Biernacka, D. BiernackiKonferencja:15th International Symposium on Principles and Practice of Declarative Programming (rok: 2013, ), Wydawca: ACMData:konferencja September 16-18Status:Opublikowana
- Axiomatizing Subtyped Delimited ContinuationsAutorzy:M. MaterzokKonferencja:Computer Science Logic (rok: 2013, ), Wydawca: Schloss Dagstuhl - Leibniz-Zentrum fuer InformatikData:konferencja September 2-5Status:Opublikowana
- Proving termination of evaluation for System F with control operatorsAutorzy:M. Biernacka, D. Biernacki, S. Lenglet, M. MaterzokKonferencja:First Workshop on Control Operators and their Semantics (rok: 2013, ), Wydawca: EPTCSData:konferencja June 24-25Status:Opublikowana
- Applicative Bisimilarities for Call-by-Name and Call-by-Value λμ-CalculusAutorzy:Dariusz Biernacki, Sergueï LengletKonferencja:30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX) (rok: 2014, ), Wydawca: ElsevierData:konferencja June 12-15Status:Opublikowana
- Logical Relations for Coherence of Effect Subtyping.Autorzy:Dariusz Biernacki, Piotr PolesiukKonferencja:Typed Lambda Calculi and Applications (rok: 2015, ), Wydawca: Schloss Dagstuhl -- Leibniz-Zentrum fuer InformatikData:konferencja July 1-3Status:Opublikowana
- Environmental Bisimulations for Delimited-Control OperatorsAutorzy:D. Biernacki, S. LengletKonferencja:11th Asian Symposium on Programming Languages and Systems (rok: 2013, ), Wydawca: SpringerData:konferencja 9-11 DecemberStatus:Opublikowana