Projects funded by the NCN


Information on the principal investigator and host institution

Information of the project and the call

Keywords

Equipment

Delete all

Structure and interpretation of programming languages in the "proofs-as-programs" paradigm

2011/03/B/ST6/00348

Keywords:

programming languages Curry-Howard isomorphism program transformation continuations control operators interactive theorem proving

Descriptors:

  • ST6_3: Software engineering, operating systems, software development methods, programming languages
  • ST6_7: Artificial intelligence, intelligent systems, multi-agent systems

Panel:

ST6 - Computer science and informatics: informatics and information systems, computer science, scientific computing, intelligent systems

Host institution :

Uniwersytet Wrocławski, Wydział Matematyki i Informatyki

woj. dolnośląskie

Other projects carried out by the institution 

Principal investigator (from the host institution):

dr Małgorzata Biernacka 

Number of co-investigators in the project: 5

Call: OPUS 2 - announced on 2011-09-15

Amount awarded: 399 220 PLN

Project start date (Y-m-d): 2012-08-31

Project end date (Y-m-d): 2016-02-29

Project duration:: 42 months (the same as in the proposal)

Project status: Project settled

Equipment purchased [PL]

  1. laptop (10 000 PLN)
  2. etui na laptopa.
  3. adapter HDMI-microHDMI, kabel HDMI.
  4. dysk twardy z etui.
  5. myszka komputerowa 3 sztuki.
  6. słuchawki nauszne 2 pary.
  7. adapter VGA.

Information in the final report

  • Publication in academic press/journals (1)
  • Articles in post-conference publications (7)
  1. Subtyping Delimited Continuations
    Authors:
    M. Materzok, D. Biernacki
    Academic press:
    Higher-Order and Symbolic Computation (rok: 2013, tom: nie dotyczy, strony: nie dotyczy), Wydawca: Springer
    Status:
    Accepted for publication
  1. A Dynamic Interpretation of the CPS Hierarchy
    Authors:
    M. Materzok, D. Biernacki
    Conference:
    10th Asian Symposium on Programming Languages and Systems (rok: 2012, ), Wydawca: Springer
    Data:
    konferencja December 11-13
    Status:
    Published
  2. An operational foundation for the tactic language of Coq
    Authors:
    W. Jedynak, M. Biernacka, D. Biernacki
    Conference:
    15th International Symposium on Principles and Practice of Declarative Programming (rok: 2013, ), Wydawca: ACM
    Data:
    konferencja September 16-18
    Status:
    Published
  3. Axiomatizing Subtyped Delimited Continuations
    Authors:
    M. Materzok
    Conference:
    Computer Science Logic (rok: 2013, ), Wydawca: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
    Data:
    konferencja September 2-5
    Status:
    Published
  4. Proving termination of evaluation for System F with control operators
    Authors:
    M. Biernacka, D. Biernacki, S. Lenglet, M. Materzok
    Conference:
    First Workshop on Control Operators and their Semantics (rok: 2013, ), Wydawca: EPTCS
    Data:
    konferencja June 24-25
    Status:
    Published
  5. Applicative Bisimilarities for Call-by-Name and Call-by-Value λμ-Calculus
    Authors:
    Dariusz Biernacki, Sergueï Lenglet
    Conference:
    30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX) (rok: 2014, ), Wydawca: Elsevier
    Data:
    konferencja June 12-15
    Status:
    Published
  6. Logical Relations for Coherence of Effect Subtyping.
    Authors:
    Dariusz Biernacki, Piotr Polesiuk
    Conference:
    Typed Lambda Calculi and Applications (rok: 2015, ), Wydawca: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
    Data:
    konferencja July 1-3
    Status:
    Published
  7. Environmental Bisimulations for Delimited-Control Operators
    Authors:
    D. Biernacki, S. Lenglet
    Conference:
    11th Asian Symposium on Programming Languages and Systems (rok: 2013, ), Wydawca: Springer
    Data:
    konferencja 9-11 December
    Status:
    Published