photo

Małgorzata Biernacka

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

[Short CV]
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@cs.uni.wroc.pl
Activities:
PEPM 2015, PC member
SOFSEM 2015, PC member
IFL 2014, PC member
TYPES 2014, PC member
LOPSTR 2011, PC member
Continuation Workshop 2011, PC member
Teaching in Fall 2014 (in Polish):
Logika dla informatyków (ćwiczenia)
Research interests:
  • logic and semantics of computation
  • reasoning and program verification in type theory
  • Curry-Howard isomorphism
  • normalization by evaluation
Publications:

An Operational Foundation for the Tactic Language of Coq.
Wojciech Jedynak, Malgorzata Biernacka, and Dariusz Biernacki.
In Ricardo Pena and Tom Shrijvers, editors, Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming (PPDP 2013), pp. 25-36, Madrid, Spain, September 2013. ACM Press. [ pdf ]

Proving Termination of Evaluation for System F with Control Operators.
Malgorzata Biernacka, Dariusz Biernacki, Serguei Lenglet, and Marek Materzok.
In U. de'Liguoro and A. Saurin, editors, Proceedings of the 1st Workshop on Control Operators and their Semantics (COS 2013), pp. 15-29, Eindhoven, The Netherlands, June 2013. EPTCS 127, 2013. [ pdf ]

Generating certified higher-order one-pass transformations.
Małgorzata Biernacka.
Manuscript. [files]

Typing Control Operators in the CPS Hierarchy.
Małgorzata Biernacka, Dariusz Biernacki and Sergueï Lenglet.
13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2011), Odense, Denmark, July 2011.

Automating Derivations of Abstract Machines from Reduction Semantics: A Generic Formalization of Refocusing in Coq.
Filip Sieczkowski, Małgorzata Biernacka and Dariusz Biernacki.
In J. Hage and M. T. Morazán, editors, Proceedings of the 22nd Symposium on Implementation and Application of Functional Languages (IFL 2010), pp. 72-88, Alphen aan den Rijn, The Netherlands, September 2010. LNCS 6647, 2011. Springer-Verlag. [Coq development]

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.
11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2009), Coimbra, Portugal, September 2009, pp. 289-300. [pdf]

A context-based approach to proving termination of evaluation.
Małgorzata Biernacka and Dariusz Biernacki.
25th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXV), Oxford, UK, April 2009. ENTCS 249, pp. 169-192, 2009. [pdf]

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: September 23, 2014