Dariusz Biernacki's home page Home Publications Students Courses

Publications

International journals and conference proceedings:

Proving Soundness of Extensional Normal-Form Bisimilarities.
Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk.
Accepted for presentation at the 33rd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII), Ljubljana, Slovenia, June 2017.
[PDF] [Coq development]

Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines.
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, and Alan Schmitt.
In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Reykjavik, Iceland, June 2017. ACM Press.
[PDF] [Extended version]

Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation.
Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk.
In Delia Kesner and Brigitte Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, pp. 9:1-9:17, Porto, Portugal, June 2016. LIPIcs 52, Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik 2016.
Best Paper Award.
[PDF] [Extended version]
An extended version invited to a special issue of Logical Methods in Computer Science (LMCS) devoted to showcase FSCD'16 papers.

Bisimulations for Delimited-Control Operators.
Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk.
This work subsumes our previous work on bisimulations for delimited-control operators (papers published at FOSSACS'12, FLOPS'12 and APLAS'13).
Accepted for publication in Information and Computation.
Available as HAL research document hal-01207112.

A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations.
Dariusz Biernacki, Olivier Danvy, and Kevin Millikin.
ACM Transactions on Programming Languages and Systems (TOPLAS), 38(1):2:1-2:25, 2015.
[PDF] [SML implementation]

Logical Relations for Coherence of Effect Subtyping.
Dariusz Biernacki and Piotr Polesiuk.
In Thorsten Altenkirch, editor, Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), pp. 107-122, Warsaw, Poland, July 2015. LIPIcs 38, 2015. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik.
[PDF] [Coq development]
An extended version invited to a special issue of Logical Methods in Computer Science (LMCS): Selected papers of the joint 26th International Conference on "Rewriting Techniques and Applications" and 13th International Conference on "Typed Lambda Calculi and Applications" RTA/TLCA 2015.

Applicative Bisimilarities for Call-by-Name and Call-by-Value λμ-Calculus.
Dariusz Biernacki and Sergueï Lenglet.
In Bart Jacobs, Alexandra Silva, and Sam Staton, editors, Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXX), pp. 49-64, Ithaca, NY, June 2014. ENTCS 308, 2014. Elsevier.
[PDF] [Extended version]

Environmental Bisimulations for Delimited-Control Operators.
Dariusz Biernacki and Sergueï Lenglet.
In Chung-chieh Shan, editor, Proceedings of the 11th Asian Symposium on Programming Languages and Systems (APLAS 2013), pp. 333-348, Melbourne, Australia, December 2013. LNCS 8301, 2013. Springer.
[PDF] [Extended version]

An Operational Foundation for the Tactic Language of Coq.
Wojciech Jedynak, Małgorzata Biernacka, and Dariusz Biernacki.
In Ricardo Peña 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]

A Dynamic Interpretation of the CPS Hierarchy.
Marek Materzok and Dariusz Biernacki.
In R. Jhala and A. Igarashi, editors, Proceedings of the 10th Asian Symposium on Programming Languages and Systems (APLAS 2012), pp. 296-311, Kyoto, Japan, December 2012. LNCS 7705, 2012. Springer.
[PDF]

Normal Form Bisimulations for Delimited-Control Operators.
Dariusz Biernacki and Sergueï Lenglet.
In T. Shrijvers and P. Thiemann, editors, Proceedings of the 11th International Symposium on Functional and Logic Programming (FLOPS 2012), pp. 47-61, Kobe, Japan, May 2012. LNCS 7294, 2012. Springer.
[PDF] [Extended version]

Applicative Bisimulations for Delimited-Control Operators.
Dariusz Biernacki and Sergueï Lenglet.
In L. Birkedal, editor, Proceedings of the 15th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2012), pp. 119-134, Tallinn, Estonia, March 2012. LNCS 7213, 2012. Springer.
[PDF] [Extended version]

Subtyping Delimited Continuations.
Marek Materzok and Dariusz Biernacki.
In M. Chakravarty, Z. Hu and O. Danvy, editors, Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011), pp. 81-93, Tokyo, Japan, September 2011. ACM Press.
[PDF] [Twelf formalization] [Haskell implementation]
An extended version accepted for publication in Higher-Order and Symbolic Computation.
[PDF]

Typing Control Operators in the CPS Hierarchy.
Małgorzata Biernacka, Dariusz Biernacki, and Sergueï Lenglet.
In P. Schneider-Kamp and M. Hanus, editors, Proceedings of the 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2011), pp. 149-160, Odense, Denmark, July 2011. ACM Press.
[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. Morazan, 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.
[PDF] [Coq development]

A Systematic Derivation of the STG Machine Verified in Coq.
Maciej Piróg and Dariusz Biernacki.
In J. Gibbons, editor, Proceedings of the 3rd ACM Haskell Symposium (Haskell 2010), pp. 25-36, Baltimore, MD, September 2010. ACM Press.
[PDF] [Coq development]

Context-based Proofs of Termination for Typed Delimited-Control Operators.
Małgorzata Biernacka and Dariusz Biernacki.
In A. Porto and F. J. López-Fraguas, editors, Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2009), pp. 289-300, Coimbra, Portugal, September 2009. ACM Press.
[PDF]

A Context-based Approach to Proving Termination of Evaluation.
Małgorzata Biernacka and Dariusz Biernacki.
In S. Abramsky, M. Mislove and C. Palamidessi, editors, Proceedings of the 25th Conference on the Mathematical Foundations of Programming Semantics (MFPS 25), pp. 169-192, Oxford, UK, April 2009. ENTCS 249, 2009.
[PDF]

Clock-directed Modular Code Generation for Synchronous Data-Flow Languages.
Dariusz Biernacki, Jean-Louis Colaço, Gregoire Hammon, and Marc Pouzet.
In K. Flautner and J. Regehr, editors, Proceedings of the 2008 ACM SIGPLAN-SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2008), pp. 121-130, Tucson, AZ, June 2008. ACM Press.
[PDF]

Clock-directed Modular Code Generation from Synchronous Block Diagrams.
Dariusz Biernacki, Jean-Louis Colaço, and Marc Pouzet.
In P. H. J. Kelly and K. Hammond, editors, Proceedings of the 2007 Workshop on Automatic Program Generation for Embedded Systems (APGES 2007), pp. 12-20, Salzburg, Austria, October 2007.
[PDF]

Formalizing Constructions of Abstract Machines for Functional Languages in Coq.
Małgorzata Biernacka and Dariusz Biernacki.
In J. Giesl, editor, Informal Proceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2007), pp. 84-99, Paris, France, June 2007.
[PDF]

On the Static and Dynamic Extents of Delimited Continuations.
Dariusz Biernacki, Olivier Danvy, and Chung-chieh Shan.
Science of Computer Programming, 60(3):274-297, 2006.
[PDF]

A Simple Proof of a Folklore Theorem about Delimited Control.
Dariusz Biernacki and Olivier Danvy.
Journal of Functional Programming, vol. 16(3):269-280, 2006. Theoretical Pearl.
[PDF]

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, 2005.
[PDF]

On the Dynamic Extent of Delimited Continuations.
Dariusz Biernacki, Olivier Danvy, and Chung-chieh Shan.
Information Processing Letters, 6(1):7-17, 2005.
[PDF]

An Operational Foundation for Delimited Continuations.
Małgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy.
In H. Thielecke, editor, Proceedings of the 4th ACM SIGPLAN Workshop on Continuations (CW'04), pp. 25-33, Venice, Italy, January 2004. Technical report CSR-04-1, Department of Computer Science, Queen Mary's College, 2004.
[PDF]

From Interpreter to Logic Engine by Defunctionalization.
Dariusz Biernacki and Olivier Danvy.
In M. Bruynooghe, editor, Proceedings of the 13th International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR 2003), pp. 141-159, Uppsala, Sweden, August 2003. LNCS 3018, 2004. Springer-Verlag.
[PDF]

A Functional Correspondence between Evaluators and Abstract Machines.
Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard.
In D. Miller, editor, Proceedings of the 5th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP 2003), pp. 8-19, Uppsala, Sweden, August 2003. ACM Press.
[PDF]

Other publications:

From Interpreter to Compiler and Virtual Machine: a Functional Derivation.
Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard.
BRICS technical report BRICS RS-03-14, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, March 2003.

Scheme Implementation of the RAM and PRAM Machines.
Dariusz Biernacki, Małgorzata Darczuk, Jacek Kisyński, Marcin Lasota, and Jerzy Mycka.
In Proceedings of the VI Lubelskie Akademickie Forum Informatyczne (LAFI 2002), Kazimierz Dolny, Poland, May 2002. Informatyka Stosowana S2/02. In Polish.

Four-Valued Logics and Relational Databases.
Dariusz Biernacki and Małgorzata Darczuk.
In Proceedings of the V Lubelskie Akademickie Forum Informatyczne (LAFI 2001), Kazimierz Dolny, Poland, May 2001. Informatyka Stosowana S2/01. In Polish.

Prolog and Artificial Intelligence.
Dariusz Biernacki, Małgorzata Darczuk, and Jacek Kisyński.
In Proceedings of the IV Lubelskie Akademickie Forum Informatyczne (LAFI 2000), Kazimierz Dolny, Poland, May 2000. Informatyka Stosowana S2/00. In Polish.

http://www.ii.uni.wroc.pl/~dabi