@misc{bockenek:hal-02069705,
  TITLE = {{Using Isabelle/UTP for the Verification of Sorting Algorithms A Case Study}},
  AUTHOR = {Bockenek, Joshua A and Lammich, Peter and Nemouchi, Yakoub and Wolff, Burkhart},
  URL = {https://easychair.org/publications/preprint/CxRV},
  NOTE = {Isabelle Workshop 2018, Colocated with Interactive Theorem Proving. As part of FLOC 2018, Oxford, GB.},
  YEAR = {2018},
  MONTH = Jul
}

@book{DBLP:books/sp/NipkowPW02,
  author    = {Tobias Nipkow and
               Lawrence C. Paulson and
               Markus Wenzel},
  title     = {Isabelle/HOL - {A} Proof Assistant for Higher-Order Logic},
  series    = {Lecture Notes in Computer Science},
  volume    = {2283},
  publisher = {Springer},
  year      = {2002},
  url       = {https://doi.org/10.1007/3-540-45949-9},
  doi       = {10.1007/3-540-45949-9},
  isbn      = {3-540-43376-7},
  timestamp = {Tue, 14 May 2019 10:00:35 +0200},
  biburl    = {https://dblp.org/rec/bib/books/sp/NipkowPW02},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/sosp/KleinEHACDEEKNSTW09,
  author    = {Gerwin Klein and
               Kevin Elphinstone and
               Gernot Heiser and
               June Andronick and
               David Cock and
               Philip Derrin and
               Dhammika Elkaduwe and
               Kai Engelhardt and
               Rafal Kolanski and
               Michael Norrish and
               Thomas Sewell and
               Harvey Tuch and
               Simon Winwood},
  title     = {seL4: formal verification of an {OS} kernel},
  booktitle = {Proceedings of the 22nd {ACM} Symposium on Operating Systems Principles
               2009, {SOSP} 2009, Big Sky, Montana, USA, October 11-14, 2009},
  pages     = {207--220},
  year      = {2009},
  crossref  = {DBLP:conf/sosp/2009},
  url       = {https://doi.org/10.1145/1629575.1629596},
  doi       = {10.1145/1629575.1629596},
  timestamp = {Tue, 06 Nov 2018 16:59:32 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/sosp/KleinEHACDEEKNSTW09},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/sosp/2009,
  editor    = {Jeanna Neefe Matthews and
               Thomas E. Anderson},
  title     = {Proceedings of the 22nd {ACM} Symposium on Operating Systems Principles
               2009, {SOSP} 2009, Big Sky, Montana, USA, October 11-14, 2009},
  publisher = {{ACM}},
  year      = {2009},
  url       = {https://doi.org/10.1145/1629575},
  doi       = {10.1145/1629575},
  isbn      = {978-1-60558-752-3},
  timestamp = {Tue, 06 Nov 2018 16:59:32 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/sosp/2009},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/tphol/CohenDHLMSST09,
  author    = {Ernie Cohen and
               Markus Dahlweid and
               Mark A. Hillebrand and
               Dirk Leinenbach and
               Michal Moskal and
               Thomas Santen and
               Wolfram Schulte and
               Stephan Tobies},
  title     = {{VCC:} {A} Practical System for Verifying Concurrent {C}},
  booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference,
               TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
  pages     = {23--42},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-03359-9_2},
  doi       = {10.1007/978-3-642-03359-9_2},
  timestamp = {Tue, 23 May 2017 01:12:08 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tphol/CohenDHLMSST09},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/cacm/Leroy09,
  author    = {Xavier Leroy},
  title     = {Formal verification of a realistic compiler},
  journal   = {Commun. {ACM}},
  volume    = {52},
  number    = {7},
  pages     = {107--115},
  year      = {2009},
  url       = {http://doi.acm.org/10.1145/1538788.1538814},
  doi       = {10.1145/1538788.1538814},
  timestamp = {Thu, 02 Jul 2009 13:36:32 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/cacm/Leroy09},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Wenzel14,
  author    = {Makarius Wenzel},
  title     = {Asynchronous User Interaction and Tool Integration in Isabelle/PIDE},
  booktitle = {Interactive Theorem Proving - 5th International Conference, {ITP}
               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
               Austria, July 14-17, 2014. Proceedings},
  pages     = {515--530},
  year      = {2014},
  crossref  = {DBLP:conf/itp/2014},
  url       = {https://doi.org/10.1007/978-3-319-08970-6\_33},
  doi       = {10.1007/978-3-319-08970-6\_33},
  timestamp = {Tue, 14 May 2019 10:00:37 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/itp/Wenzel14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/itp/2014,
  editor    = {Gerwin Klein and
               Ruben Gamboa},
  title     = {Interactive Theorem Proving - 5th International Conference, {ITP}
               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
               Austria, July 14-17, 2014. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8558},
  publisher = {Springer},
  year      = {2014},
  url       = {https://doi.org/10.1007/978-3-319-08970-6},
  doi       = {10.1007/978-3-319-08970-6},
  isbn      = {978-3-319-08969-0},
  timestamp = {Tue, 14 May 2019 10:00:37 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/itp/2014},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:journals/corr/Wenzel14,
  author    = {Makarius Wenzel},
  title     = {System description: Isabelle/jEdit in 2014},
  booktitle = {Proceedings Eleventh Workshop on User Interfaces for Theorem Provers,
               {UITP} 2014, Vienna, Austria, 17th July 2014.},
  pages     = {84--94},
  year      = {2014},
  crossref  = {DBLP:journals/corr/BenzmullerP14},
  url       = {https://doi.org/10.4204/EPTCS.167.10},
  doi       = {10.4204/EPTCS.167.10},
  timestamp = {Wed, 12 Sep 2018 01:05:15 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/Wenzel14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:journals/corr/BenzmullerP14,
  editor    = {Christoph Benzm{\"{u}}ller and
               Bruno {Woltzenlogel Paleo}},
  title     = {Proceedings Eleventh Workshop on User Interfaces for Theorem Provers,
               {UITP} 2014, Vienna, Austria, 17th July 2014},
  series    = {{EPTCS}},
  volume    = {167},
  year      = {2014},
  url       = {https://doi.org/10.4204/EPTCS.167},
  doi       = {10.4204/EPTCS.167},
  timestamp = {Wed, 12 Sep 2018 01:05:15 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/BenzmullerP14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/mkm/BarrasGHRTWW13,
  author    = {Bruno Barras and
               Lourdes Del Carmen Gonz{\'{a}}lez{-}Huesca and
               Hugo Herbelin and
               Yann R{\'{e}}gis{-}Gianas and
               Enrico Tassi and
               Makarius Wenzel and
               Burkhart Wolff},
  title     = {Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving
               Systems},
  booktitle = {Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems
               and Projects 2013, Held as Part of {CICM} 2013, Bath, UK, July 8-12,
               2013. Proceedings},
  pages     = {359--363},
  year      = {2013},
  crossref  = {DBLP:conf/mkm/2013},
  url       = {https://doi.org/10.1007/978-3-642-39320-4\_29},
  doi       = {10.1007/978-3-642-39320-4\_29},
  timestamp = {Sun, 02 Jun 2019 21:17:34 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/mkm/BarrasGHRTWW13},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/mkm/2013,
  editor    = {Jacques Carette and
               David Aspinall and
               Christoph Lange and
               Petr Sojka and
               Wolfgang Windsteiger},
  title     = {Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems
               and Projects 2013, Held as Part of {CICM} 2013, Bath, UK, July 8-12,
               2013. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7961},
  publisher = {Springer},
  year      = {2013},
  url       = {https://doi.org/10.1007/978-3-642-39320-4},
  doi       = {10.1007/978-3-642-39320-4},
  isbn      = {978-3-642-39319-8},
  timestamp = {Sun, 02 Jun 2019 21:17:34 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/mkm/2013},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/LammichW19,
  author    = {Peter Lammich and
               Simon Wimmer},
  title     = {{IMP2} - Simple Program Verification in Isabelle/HOL},
  journal   = {Archive of Formal Proofs},
  volume    = {2019},
  year      = {2019},
  url       = {https://www.isa-afp.org/entries/IMP2.html},
  timestamp = {Mon, 20 May 2019 11:45:07 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/afp/LammichW19},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@misc{frama-c-home-page,
  title = {The Frama-C Home Page},
  author = {CEA LIST},
  year = 2019,
  month = jan,
  day = 10,
  url = {https://frama-c.com},
  note = {Accessed \DTMdate{2019-03-24}}
}

@inproceedings{DBLP:conf/fm/LeinenbachS09,
  author    = {Dirk Leinenbach and Thomas Santen},
  title     = {Verifying the Microsoft Hyper-V Hypervisor with {VCC}},
  booktitle = {{FM} 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands,
               November 2-6, 2009. Proceedings},
  pages     = {806--809},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-05089-3_51},
  doi       = {10.1007/978-3-642-05089-3_51},
  timestamp = {Mon, 22 May 2017 17:11:19 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/fm/LeinenbachS09},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/tap/Keller18,
  author    = {Chantal Keller},
  title     = {Tactic Program-Based Testing and Bounded Verification in Isabelle/HOL},
  booktitle = {Tests and Proofs - 12th International Conference, {TAP} 2018, Held
               as Part of {STAF} 2018, Toulouse, France, June 27-29, 2018, Proceedings},
  pages     = {103--119},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-319-92994-1\_6},
  doi       = {10.1007/978-3-319-92994-1\_6},
  timestamp = {Mon, 18 Jun 2018 13:57:50 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tap/Keller18},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/AissatVW16,
  author    = {Romain A{\"{\i}}ssat and
               Fr{\'{e}}d{\'{e}}ric Voisin and
               Burkhart Wolff},
  title     = {Infeasible Paths Elimination by Symbolic Execution Techniques - Proof
               of Correctness and Preservation of Paths},
  booktitle = {Interactive Theorem Proving - 7th International Conference, {ITP}
               2016, Nancy, France, August 22-25, 2016, Proceedings},
  pages     = {36--51},
  year      = {2016},
  url       = {https://doi.org/10.1007/978-3-319-43144-4\_3},
  doi       = {10.1007/978-3-319-43144-4\_3},
  timestamp = {Thu, 17 Aug 2017 16:22:01 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/itp/AissatVW16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/tocs/KleinAEMSKH14,
  author    = {Gerwin Klein and
               June Andronick and
               Kevin Elphinstone and
               Toby C. Murray and
               Thomas Sewell and
               Rafal Kolanski and
               Gernot Heiser},
  title     = {Comprehensive formal verification of an {OS} microkernel},
  journal   = {{ACM} Trans. Comput. Syst.},
  volume    = {32},
  number    = {1},
  pages     = {2:1--2:70},
  year      = {2014},
  url       = {http://doi.acm.org/10.1145/2560537},
  doi       = {10.1145/2560537},
  timestamp = {Tue, 03 Jan 2017 11:51:57 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/tocs/KleinAEMSKH14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/pldi/GreenawayLAK14,
  author    = {David Greenaway and
               Japheth Lim and
               June Andronick and
               Gerwin Klein},
  title     = {Don't sweat the small stuff: formal verification of {C} code without
               the pain},
  booktitle = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation,
               {PLDI} '14, Edinburgh, United Kingdom - June 09 - 11, 2014},
  pages     = {429--439},
  year      = {2014},
  url       = {http://doi.acm.org/10.1145/2594291.2594296},
  doi       = {10.1145/2594291.2594296},
  timestamp = {Tue, 20 Dec 2016 10:12:01 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/pldi/GreenawayLAK14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/mkm/BruckerACW18,
  author    = {Achim D. Brucker and
               Idir A{\"{\i}}t{-}Sadoune and
               Paolo Crisafulli and
               Burkhart Wolff},
  title     = {Using the Isabelle Ontology Framework - Linking the Formal with the
               Informal},
  booktitle = {Intelligent Computer Mathematics - 11th International Conference,
               {CICM} 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings},
  pages     = {23--38},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-319-96812-4\_3},
  doi       = {10.1007/978-3-319-96812-4\_3},
  timestamp = {Sat, 11 Aug 2018 00:57:41 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/mkm/BruckerACW18},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/TuongW15,
  author    = {Fr{\'{e}}d{\'{e}}ric Tuong and
               Burkhart Wolff},
  title     = {A Meta-Model for the Isabelle {API}},
  journal   = {Archive of Formal Proofs},
  volume    = {2015},
  year      = {2015},
  url       = {https://www.isa-afp.org/entries/Isabelle\_Meta\_Model.shtml},
  timestamp = {Mon, 07 Jan 2019 11:16:33 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/afp/TuongW15},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/tphol/WinwoodKSACN09,
  author    = {Simon Winwood and
               Gerwin Klein and
               Thomas Sewell and
               June Andronick and
               David Cock and
               Michael Norrish},
  title     = {Mind the Gap},
  booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference,
               TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
  pages     = {500--515},
  year      = {2009},
  crossref  = {DBLP:conf/tphol/2009},
  url       = {https://doi.org/10.1007/978-3-642-03359-9\_34},
  doi       = {10.1007/978-3-642-03359-9\_34},
  timestamp = {Fri, 02 Nov 2018 09:49:05 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/tphol/WinwoodKSACN09},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/tphol/2009,
  editor    = {Stefan Berghofer and
               Tobias Nipkow and
               Christian Urban and
               Makarius Wenzel},
  title     = {Theorem Proving in Higher Order Logics, 22nd International Conference,
               TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {5674},
  publisher = {Springer},
  year      = {2009},
  url       = {https://doi.org/10.1007/978-3-642-03359-9},
  doi       = {10.1007/978-3-642-03359-9},
  isbn      = {978-3-642-03358-2},
  timestamp = {Tue, 23 May 2017 01:12:08 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tphol/2009},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/afp/BruckerTW14,
  author    = {Achim D. Brucker and
               Fr{\'{e}}d{\'{e}}ric Tuong and
               Burkhart Wolff},
  title     = {Featherweight {OCL:} {A} Proposal for a Machine-Checked Formal Semantics
               for {OCL} 2.5},
  journal   = {Archive of Formal Proofs},
  volume    = {2014},
  year      = {2014},
  url       = {https://www.isa-afp.org/entries/Featherweight\_OCL.shtml},
  timestamp = {Mon, 07 Jan 2019 11:16:33 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/afp/BruckerTW14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/tacas/SananZHZTL17,
  author    = {David San{\'{a}}n and
               Yongwang Zhao and
               Zhe Hou and
               Fuyuan Zhang and
               Alwen Tiu and
               Yang Liu},
  title     = {CSimpl: {A} Rely-Guarantee-Based Framework for Verifying Concurrent
               Programs},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
               - 23rd International Conference, {TACAS} 2017, Held as Part of the
               European Joint Conferences on Theory and Practice of Software, {ETAPS}
               2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part {I}},
  pages     = {481--498},
  year      = {2017},
  crossref  = {DBLP:conf/tacas/2017-1},
  url       = {https://doi.org/10.1007/978-3-662-54577-5\_28},
  doi       = {10.1007/978-3-662-54577-5\_28},
  timestamp = {Mon, 18 Sep 2017 08:38:37 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tacas/SananZHZTL17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/tacas/2017-1,
  editor    = {Axel Legay and
               Tiziana Margaria},
  title     = {Tools and Algorithms for the Construction and Analysis of Systems
               - 23rd International Conference, {TACAS} 2017, Held as Part of the
               European Joint Conferences on Theory and Practice of Software, {ETAPS}
               2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part {I}},
  series    = {Lecture Notes in Computer Science},
  volume    = {10205},
  year      = {2017},
  url       = {https://doi.org/10.1007/978-3-662-54577-5},
  doi       = {10.1007/978-3-662-54577-5},
  isbn      = {978-3-662-54576-8},
  timestamp = {Wed, 24 May 2017 08:28:32 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tacas/2017-1},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/HouSTL17,
  author    = {Zhe Hou and
               David San{\'{a}}n and
               Alwen Tiu and
               Yang Liu},
  title     = {Proof Tactics for Assertions in Separation Logic},
  booktitle = {Interactive Theorem Proving - 8th International Conference, {ITP}
               2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings},
  pages     = {285--303},
  year      = {2017},
  crossref  = {DBLP:conf/itp/2017},
  url       = {https://doi.org/10.1007/978-3-319-66107-0\_19},
  doi       = {10.1007/978-3-319-66107-0\_19},
  timestamp = {Mon, 18 Sep 2017 08:38:37 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/itp/HouSTL17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/itp/2017,
  editor    = {Mauricio Ayala{-}Rinc{\'{o}}n and
               C{\'{e}}sar A. Mu{\~{n}}oz},
  title     = {Interactive Theorem Proving - 8th International Conference, {ITP}
               2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {10499},
  publisher = {Springer},
  year      = {2017},
  url       = {https://doi.org/10.1007/978-3-319-66107-0},
  doi       = {10.1007/978-3-319-66107-0},
  isbn      = {978-3-319-66106-3},
  timestamp = {Wed, 06 Sep 2017 14:53:52 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/itp/2017},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/sigbed/CarrascosaCMBC14,
  author    = {E. Carrascosa and
               Javier Coronel and
               Miguel Masmano and
               Patricia Balbastre and
               Alfons Crespo},
  title     = {XtratuM hypervisor redesign for {LEON4} multicore processor},
  journal   = {{SIGBED} Review},
  volume    = {11},
  number    = {2},
  pages     = {27--31},
  year      = {2014},
  url       = {https://doi.org/10.1145/2668138.2668142},
  doi       = {10.1145/2668138.2668142},
  timestamp = {Tue, 06 Nov 2018 12:51:31 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/sigbed/CarrascosaCMBC14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/cacm/Earley70,
  author    = {Jay Earley},
  title     = {An Efficient Context-Free Parsing Algorithm},
  journal   = {Commun. {ACM}},
  volume    = {13},
  number    = {2},
  pages     = {94--102},
  year      = {1970},
  url       = {https://doi.org/10.1145/362007.362035},
  doi       = {10.1145/362007.362035},
  timestamp = {Wed, 14 Nov 2018 10:22:30 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/cacm/Earley70},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
   
@article{DBLP:journals/jfp/Hutton92,
  author    = {Graham Hutton},
  title     = {Higher-Order Functions for Parsing},
  journal   = {J. Funct. Program.},
  volume    = {2},
  number    = {3},
  pages     = {323--343},
  year      = {1992},
  url       = {https://doi.org/10.1017/S0956796800000411},
  doi       = {10.1017/S0956796800000411},
  timestamp = {Sat, 27 May 2017 14:24:34 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/jfp/Hutton92},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{TuongWolff19,
  author    = {Fr{\'{e}}d{\'{e}}ric Tuong and
               Burkhart Wolff},
  title     = {Deeply Integrating {C11} Code Support into Isabelle/PIDE},
  booktitle = {Formal IDE - 5th International Workshop, {F-IDE}
               2019, Porto, Portugal, October 7, 2019. Proceedings},
  year      = {2019},
  url       = {https://gitlri.lri.fr/ftuong/isabelle_c},
}

@inproceedings{DBLP:conf/ictac/FosterZW16,
  author    = {Simon Foster and
               Frank Zeyda and
               Jim Woodcock},
  title     = {Unifying Heterogeneous State-Spaces with Lenses},
  booktitle = {Theoretical Aspects of Computing - {ICTAC} 2016 - 13th International
               Colloquium, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings},
  pages     = {295--314},
  year      = {2016},
  crossref  = {DBLP:conf/ictac/2016},
  url       = {https://doi.org/10.1007/978-3-319-46750-4\_17},
  doi       = {10.1007/978-3-319-46750-4\_17},
  timestamp = {Tue, 14 May 2019 10:00:38 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/ictac/FosterZW16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/ictac/2016,
  editor    = {Augusto Sampaio and
               Farn Wang},
  title     = {Theoretical Aspects of Computing - {ICTAC} 2016 - 13th International
               Colloquium, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9965},
  year      = {2016},
  url       = {https://doi.org/10.1007/978-3-319-46750-4},
  doi       = {10.1007/978-3-319-46750-4},
  isbn      = {978-3-319-46749-8},
  timestamp = {Tue, 14 May 2019 10:00:38 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/ictac/2016},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@phdthesis{Foster2009BidirectionalPL,
  author    = {John Nathan Foster},
  title     = {Bidirectional programming languages},
  school    = {University of Pennsylvania},
  year      = {2009},
  url       = {https://repository.upenn.edu/edissertations/56/}
}

@article{DBLP:journals/toplas/FosterGMPS07,
  author    = {J. Nathan Foster and
               Michael B. Greenwald and
               Jonathan T. Moore and
               Benjamin C. Pierce and
               Alan Schmitt},
  title     = {Combinators for bidirectional tree transformations: {A} linguistic
               approach to the view-update problem},
  journal   = {{ACM} Trans. Program. Lang. Syst.},
  volume    = {29},
  number    = {3},
  pages     = {17},
  year      = {2007},
  url       = {https://doi.org/10.1145/1232420.1232424},
  doi       = {10.1145/1232420.1232424},
  timestamp = {Tue, 06 Nov 2018 12:51:29 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/toplas/FosterGMPS07},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
