photo

Małgorzata Biernacka

Current position: Assistant Professor, Institute of Computer Science, University of Wroclaw

Contact info:
Institute of Computer Science
University of Wroclaw
ul. Joliot-Curie 15
50-383 Wroclaw
Poland

Office: 339
Phone: (+48) 71 375 7836

E-mail: mabi@ii.uni.wroc.pl
Teaching in Spring 2010 (in Polish):
Obliczenia i wnioskowanie w systemie Coq
Programowanie (grupa rozszerzona)
Kurs WWW
Research interests:
  • logic and semantics of computation
  • reasoning and program verification in type theory
  • Curry-Howard isomorphism
  • normalization by evaluation
Publications:

Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part II: Reduction Semantics and Abstract Machines.
Małgorzata Biernacka and Olivier Danvy.
Festschrift in the honour of Peter Mosses. Lecture Notes in Computer Science, 5700:162-185, September 2009.

Context-based proofs of termination for typed delimited-control operators.
Małgorzata Biernacka and Dariusz Biernacki.
PPDP, Coimbra, Portugal, September 2009.

A context-based approach to proving termination of evaluation.
Małgorzata Biernacka and Dariusz Biernacki.
MFPS XXV, Oxford, UK, April 2009.

Towards compatible and interderivable semantic specifications for the Scheme programming language, part II: reduction semantics and abstract machines.
Małgorzata Biernacka and Olivier Danvy.
2008 Workshop on Scheme and Functional Programming.
Available in the workshop proceedings: [PDF].


Formalization of the proof of weak head normalization for System T and its extracted evaluator (an instance of normalization by evaluation).
In preparation. [Coq development] available (extends parts of Schwichtenberg and Letouzey's development for strong normalization for the simply typed lambda calculus: [Coq contribution]) .


Formalizing Constructions of Abstract Machines for Functional Languages in Coq.
Małgorzata Biernacka and Dariusz Biernacki.
(the article is accompanied by [Coq development].)

Preliminary results presented at 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2007), Paris, June 2007.

A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines.
Małgorzata Biernacka and Olivier Danvy.
Theoretical Computer Science, 375:76-108, 2007.

Available as a BRICS technical report BRICS RS-06-18, Dept. of Computer Science, University of Aarhus, Denmark, December 2006.
Available version: [pdf] | [ps]

A Concrete Framework for Environment Machines.
Małgorzata Biernacka and Olivier Danvy.
ACM Transactions on Computational Logic, 9(1):6, 2007.

Available as a BRICS technical report BRICS RS-06-3, Dept. of Computer Science, University of Aarhus, Denmark, February 2006.

An Operational Foundation for Delimited Continuations in the CPS Hierarchy.
Małgorzata Biernacka, Dariusz Biernacki and Olivier Danvy.
Logical Methods in Computer Science, 1(2:5):1-39, November 2005.

Program Extraction from Proofs of Weak Head Normalization.
Małgorzata Biernacka, Olivier Danvy and Kristian Støvring.
In M. Escardò, editor, Proceedings of the 21st Conference on the Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science, Birmingham, UK, May 2005. Elsevier Science Publishers.

Available version: [pdf] | [ps]

An Operational Foundation for Delimited Continuations.
Małgorzata Biernacka, Dariusz Biernacki and Olivier Danvy.
In Hayo Thielecke, editor, Proceedings of the Fourth ACM SIGPLAN Workshop on Continuations, Technical report CSR-04-1, Department of Computer Science, Queen Mary's College, pages 25-33, Venice, Italy, January 2004.

Available as a BRICS technical report BRICS RS-03-41, Dept. of Computer Science, University of Aarhus, Denmark, December 2003.
C'est avec la logique que nous prouvons et avec l'intuition que nous trouvons.
Henri Poincaré

Never lose a holy curiosity.
Albert Einstein

Science... Never solves a problem without creating ten more.
George Bernard Shaw
Last modified: March 2, 2010