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@cs.uni.wroc.pl
Research interests:
  • logic and semantics of computation
  • reasoning and program verification in type theory
  • Curry-Howard isomorphism
  • normalization by evaluation
Publications:
An Abstract Machine for Strong Call by Value.
Małgorzata Biernacka, Dariusz Biernacki, Witold Charatonik, Tomasz Drab.
Accepted for publication at APLAS 2020.
Deriving an Abstract Machine for Strong Call by Need
Małgorzata Biernacka, Witold Charatonik.
FSCD 2019, Dortmund, Germany, June 2019.

Generalized Refocusing: from Hybrid Strategies to Abstract Machines
Małgorzata Biernacka, Witold Charatonik, Klara Zielińska.
FSCD 2017, Oxford, UK, September 2017.

Fully Abstract Encodings of lambda-Calculus in HOCore through Abstract Machines.
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous and Alan Schmitt.
LICS 2017, Reykjavik, Iceland, June 2017. [ pdf ]

Generalized Refocusing: a Formalization in Coq.
Klara Zielińska and Małgorzata Biernacka.
Presented at 11th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2016), Porto, Portugal, June 2016. [ pdf ]

Certification of higher-order one-pass CPS transformations.
Małgorzata Biernacka.
Manuscript. [Coq development]

An Operational Foundation for the Tactic Language of Coq.
Wojciech Jedynak, Małgorzata 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.
Małgorzata Biernacka, Dariusz Biernacki, Sergueï 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]

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. [ pdf ]

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. [pdf] [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. [ pdf ]

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).


Formalizing Constructions of Abstract Machines for Functional Languages in Coq.
Małgorzata Biernacka and Dariusz Biernacki.
Preliminary results presented at 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2007), Paris, June 2007. [ pdf ]

(The article has been superseded by the IFL 2010 paper "Automating Derivations of Abstract Machines from Reduction Semantics: A Generic Formalization of Refocusing in Coq.")

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

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

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

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. [ pdf ]

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. [ pdf ]

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: December 18, 2019