Powell, Thomas Proofs as stateful programs: a first-order logic with abstract Hoare triples, and an interpretation into an imperative language. (English) Zbl 07814915 Log. Methods Comput. Sci. 20, No. 1, Paper No. 7, 32 p. (2024). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{T. Powell}, Log. Methods Comput. Sci. 20, No. 1, Paper No. 7, 32 p. (2024; Zbl 07814915) Full Text: DOI arXiv
Huang, Kangjing; Qiu, Xiaokang Bootstrapping library-based synthesis. (English) Zbl 1524.68091 Singh, Gagandeep (ed.) et al., Static analysis. 29th international symposium, SAS 2022, Auckland, New Zealand, December 5–7, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13790, 272-298 (2022). MSC: 68N30 68N15 PDFBibTeX XMLCite \textit{K. Huang} and \textit{X. Qiu}, Lect. Notes Comput. Sci. 13790, 272--298 (2022; Zbl 1524.68091) Full Text: DOI
Ekici, Burak Formal categorical reasoning. (English) Zbl 1524.68429 Turk. J. Math. 46, No. 4, 1538-1552 (2022). MSC: 68V20 03G30 18C50 68V15 PDFBibTeX XMLCite \textit{B. Ekici}, Turk. J. Math. 46, No. 4, 1538--1552 (2022; Zbl 1524.68429) Full Text: DOI
Annenkov, Danil; Milo, Mikkel; Nielsen, Jakob Botsch; Spitters, Bas Extracting functional programs from Coq, in Coq. (English) Zbl 07581654 J. Funct. Program. 32, Paper No. e11, 60 p. (2022). MSC: 68N18 PDFBibTeX XMLCite \textit{D. Annenkov} et al., J. Funct. Program. 32, Paper No. e11, 60 p. (2022; Zbl 07581654) Full Text: DOI arXiv
Affeldt, Reynald; Garrigue, Jacques; Nowak, David; Saikawa, Takafumi A trustful monad for axiomatic reasoning with probability and nondeterminism. (English) Zbl 1493.03004 J. Funct. Program. 31, Paper No. e17, 38 p. (2021). Reviewer: Alexandre Goy (Lyon) MSC: 03B70 03B35 68N18 68V15 PDFBibTeX XMLCite \textit{R. Affeldt} et al., J. Funct. Program. 31, Paper No. e17, 38 p. (2021; Zbl 1493.03004) Full Text: DOI arXiv
Pit-Claudel, Clément; Wang, Peng; Delaware, Benjamin; Gross, Jason; Chlipala, Adam Extensible extraction of efficient imperative programs with foreign functions, manually managed memory, and proofs. (English) Zbl 07614665 Peltier, Nicolas (ed.) et al., Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1–4, 2020. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12167, 119-137 (2020). MSC: 68V15 PDFBibTeX XMLCite \textit{C. Pit-Claudel} et al., Lect. Notes Comput. Sci. 12167, 119--137 (2020; Zbl 07614665) Full Text: DOI
Costea, Andreea; Zhu, Amy; Polikarpova, Nadia; Sergey, Ilya Concise read-only specifications for better synthesis of programs with pointers. (English) Zbl 1508.68056 Müller, Peter (ed.), Programming languages and systems. 29th European symposium on programming, ESOP 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12075, 141-168 (2020). MSC: 68N30 PDFBibTeX XMLCite \textit{A. Costea} et al., Lect. Notes Comput. Sci. 12075, 141--168 (2020; Zbl 1508.68056) Full Text: DOI arXiv
Genovese, Fabrizio; Gryzlov, Alex; Herold, Jelle; Knispel, Andre; Perone, Marco; Post, Erik; Videla, André idris-ct: a library to do category theory in Idris. (English) Zbl 07453982 Baez, John (ed.) et al., Proceedings of the applied category theory 2019, ACT 2019, University of Oxford, UK, July 15–19, 2019. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 323, 246-254 (2020). MSC: 68-XX 18-XX PDFBibTeX XMLCite \textit{F. Genovese} et al., Electron. Proc. Theor. Comput. Sci. (EPTCS) 323, 246--254 (2020; Zbl 07453982) Full Text: arXiv Link
Sozeau, Matthieu; Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Forster, Yannick; Kunze, Fabian; Malecha, Gregory; Tabareau, Nicolas; Winterhalter, Théo The MetaCoq project. (English) Zbl 1468.68075 J. Autom. Reasoning 64, No. 5, 947-999 (2020). MSC: 68N30 68V15 PDFBibTeX XMLCite \textit{M. Sozeau} et al., J. Autom. Reasoning 64, No. 5, 947--999 (2020; Zbl 1468.68075) Full Text: DOI
Ekici, Burak; Kaliszyk, Cezary Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq. (English) Zbl 1474.68455 Math. Comput. Sci. 14, No. 3, 533-549 (2020). MSC: 68V20 18A15 18A40 18C20 68N30 PDFBibTeX XMLCite \textit{B. Ekici} and \textit{C. Kaliszyk}, Math. Comput. Sci. 14, No. 3, 533--549 (2020; Zbl 1474.68455) Full Text: DOI
Darais, David; Van Horn, David Constructive Galois connections. (English) Zbl 1493.68104 J. Funct. Program. 29, Paper No. e11, 60 p. (2019). MSC: 68N30 06A15 68N18 68Q55 68V15 PDFBibTeX XMLCite \textit{D. Darais} and \textit{D. Van Horn}, J. Funct. Program. 29, Paper No. e11, 60 p. (2019; Zbl 1493.68104) Full Text: DOI arXiv
Lammich, Peter; Lochbihler, Andreas Automatic refinement to efficient data structures: a comparison of two approaches. (English) Zbl 1459.68228 J. Autom. Reasoning 63, No. 1, 53-94 (2019). MSC: 68V15 68P05 PDFBibTeX XMLCite \textit{P. Lammich} and \textit{A. Lochbihler}, J. Autom. Reasoning 63, No. 1, 53--94 (2019; Zbl 1459.68228) Full Text: DOI
Lammich, Peter Refinement to imperative HOL. (English) Zbl 1465.68291 J. Autom. Reasoning 62, No. 4, 481-503 (2019). MSC: 68V15 68P05 68V20 68W01 PDFBibTeX XMLCite \textit{P. Lammich}, J. Autom. Reasoning 62, No. 4, 481--503 (2019; Zbl 1465.68291) Full Text: DOI Link
Charguéraud, Arthur; Pottier, François Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. (English) Zbl 1468.68120 J. Autom. Reasoning 62, No. 3, 331-365 (2019). MSC: 68Q60 03B70 68N18 68P05 68V20 PDFBibTeX XMLCite \textit{A. Charguéraud} and \textit{F. Pottier}, J. Autom. Reasoning 62, No. 3, 331--365 (2019; Zbl 1468.68120) Full Text: DOI HAL
Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques. (English) Zbl 1395.68246 J. Symb. Comput. 90, 3-41 (2019). MSC: 68T15 68P10 PDFBibTeX XMLCite \textit{I. Drămnesc} et al., J. Symb. Comput. 90, 3--41 (2019; Zbl 1395.68246) Full Text: DOI HAL
Yang, Kai; Duan, Zhenhua; Tian, Cong; Zhang, Nan A compiler for MSVL and its applications. (English) Zbl 1407.68096 Theor. Comput. Sci. 749, 2-16 (2018). MSC: 68N20 68Q60 68T20 PDFBibTeX XMLCite \textit{K. Yang} et al., Theor. Comput. Sci. 749, 2--16 (2018; Zbl 1407.68096) Full Text: DOI
Dagand, Pierre-Évariste; Tabareau, Nicolas; Tanter, Éric Foundations of dependent interoperability. (English) Zbl 1476.68051 J. Funct. Program. 28, Paper No. e9, 44 p. (2018). MSC: 68N18 68N30 68Q55 PDFBibTeX XMLCite \textit{P.-É. Dagand} et al., J. Funct. Program. 28, Paper No. e9, 44 p. (2018; Zbl 1476.68051) Full Text: DOI
Dams, Dennis; Grumberg, Orna Abstraction and abstraction refinement. (English) Zbl 1392.68244 Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 385-419 (2018). MSC: 68Q60 PDFBibTeX XMLCite \textit{D. Dams} and \textit{O. Grumberg}, in: Handbook of model checking. Cham: Springer. 385--419 (2018; Zbl 1392.68244) Full Text: DOI
Hóu, Zhé; Sanán, David; Tiu, Alwen; Liu, Yang Proof tactics for assertions in separation logic. (English) Zbl 1483.03004 Ayala-Rincón, Mauricio (ed.) et al., Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10499, 285-303 (2017). MSC: 03B35 03B70 68V15 PDFBibTeX XMLCite \textit{Z. Hóu} et al., Lect. Notes Comput. Sci. 10499, 285--303 (2017; Zbl 1483.03004) Full Text: DOI Link
Slama, Franck; Brady, Edwin Automatically proving equivalence by type-safe reflection. (English) Zbl 1367.68257 Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 40-55 (2017). MSC: 68T15 68N30 PDFBibTeX XMLCite \textit{F. Slama} and \textit{E. Brady}, Lect. Notes Comput. Sci. 10383, 40--55 (2017; Zbl 1367.68257) Full Text: DOI Link
Guéneau, Armaël; Myreen, Magnus O.; Kumar, Ramana; Norrish, Michael Verified characteristic formulae for CakeML. (English) Zbl 1485.68030 Yang, Hongseok (ed.), Programming languages and systems. 26th European symposium on programming, ESOP 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 10201, 584-610 (2017). MSC: 68N15 68N18 68N30 PDFBibTeX XMLCite \textit{A. Guéneau} et al., Lect. Notes Comput. Sci. 10201, 584--610 (2017; Zbl 1485.68030) Full Text: DOI
Roe, Kenneth; Smith, Scott Coqpie: an IDE aimed at improving proof development productivity (rough diamond). (English) Zbl 1478.68437 Blanchette, Jasmin Christian (ed.) et al., Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9807, 491-499 (2016). MSC: 68V15 PDFBibTeX XMLCite \textit{K. Roe} and \textit{S. Smith}, Lect. Notes Comput. Sci. 9807, 491--499 (2016; Zbl 1478.68437) Full Text: DOI
Malecha, Gregory; Bengtson, Jesper Extensible and efficient automation through reflective tactics. (English) Zbl 1335.68234 Thiemann, Peter (ed.), Programming languages and systems. 25th European symposium on programming, ESOP 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-49497-4/pbk; 978-3-662-49498-1/ebook). Lecture Notes in Computer Science 9632, 532-559 (2016). MSC: 68T15 PDFBibTeX XMLCite \textit{G. Malecha} and \textit{J. Bengtson}, Lect. Notes Comput. Sci. 9632, 532--559 (2016; Zbl 1335.68234) Full Text: DOI
Swierstra, Wouter; Alpuim, Joao From proposition to program. Embedding the refinement calculus in Coq. (English) Zbl 1475.68458 Kiselyov, Oleg (ed.) et al., Functional and logic programming. 13th international symposium, FLOPS 2016, Kochi, Japan, March 4–6, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9613, 29-44 (2016). MSC: 68V20 68N18 68Q60 PDFBibTeX XMLCite \textit{W. Swierstra} and \textit{J. Alpuim}, Lect. Notes Comput. Sci. 9613, 29--44 (2016; Zbl 1475.68458) Full Text: DOI
Blot, Arthur; Dagand, Pierre-Évariste; Lawall, Julia From sets to bits in Coq. (English) Zbl 1475.68455 Kiselyov, Oleg (ed.) et al., Functional and logic programming. 13th international symposium, FLOPS 2016, Kochi, Japan, March 4–6, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9613, 12-28 (2016). MSC: 68V20 PDFBibTeX XMLCite \textit{A. Blot} et al., Lect. Notes Comput. Sci. 9613, 12--28 (2016; Zbl 1475.68455) Full Text: DOI
Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor Mtac: a monad for typed tactic programming in Coq. (English) Zbl 1420.68189 J. Funct. Program. 25, Paper No. e12, 59 p. (2015). MSC: 68T15 68N30 PDFBibTeX XMLCite \textit{B. Ziliani} et al., J. Funct. Program. 25, Paper No. e12, 59 p. (2015; Zbl 1420.68189) Full Text: DOI
Reus, Bernhard; Charlton, Nathaniel; Horsfall, Ben Symbolic execution proofs for higher order store programs. (English) Zbl 1356.68145 J. Autom. Reasoning 54, No. 3, 199-284 (2015). MSC: 68Q60 03B70 68T15 PDFBibTeX XMLCite \textit{B. Reus} et al., J. Autom. Reasoning 54, No. 3, 199--284 (2015; Zbl 1356.68145) Full Text: DOI Link
Hölzl, Johannes; Lochbihler, Andreas; Traytel, Dmitriy A formalized hierarchy of probabilistic system types. Proof pearl. (English) Zbl 1465.68199 Urban, Christian (ed.) et al., Interactive theorem proving. 6th international conference, ITP 2015, Nanjing, China, August 24–27, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9236, 203-220 (2015). MSC: 68Q87 68Q65 68V20 PDFBibTeX XMLCite \textit{J. Hölzl} et al., Lect. Notes Comput. Sci. 9236, 203--220 (2015; Zbl 1465.68199) Full Text: DOI
Charguéraud, Arthur; Pottier, François Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. (English) Zbl 1465.68172 Urban, Christian (ed.) et al., Interactive theorem proving. 6th international conference, ITP 2015, Nanjing, China, August 24–27, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9236, 137-153 (2015). MSC: 68Q60 03B70 68N19 68P05 68V20 PDFBibTeX XMLCite \textit{A. Charguéraud} and \textit{F. Pottier}, Lect. Notes Comput. Sci. 9236, 137--153 (2015; Zbl 1465.68172) Full Text: DOI HAL
Kokke, Pepijn; Swierstra, Wouter Auto in Agda. Programming proof search using reflection. (English) Zbl 1432.68063 Hinze, Ralf (ed.) et al., Mathematics of program construction. 12th international conference, MPC 2015, Königswinter, Germany, June 29 – July 1, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9129, 276-301 (2015). MSC: 68N18 68V15 PDFBibTeX XMLCite \textit{P. Kokke} and \textit{W. Swierstra}, Lect. Notes Comput. Sci. 9129, 276--301 (2015; Zbl 1432.68063) Full Text: DOI
Dongol, Brijesh; Gomes, Victor B. F.; Struth, Georg A program construction and verification tool for separation logic. (English) Zbl 1432.68071 Hinze, Ralf (ed.) et al., Mathematics of program construction. 12th international conference, MPC 2015, Königswinter, Germany, June 29 – July 1, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9129, 137-158 (2015). MSC: 68N30 03B70 68Q60 68V15 PDFBibTeX XMLCite \textit{B. Dongol} et al., Lect. Notes Comput. Sci. 9129, 137--158 (2015; Zbl 1432.68071) Full Text: DOI arXiv Link
Braghin, Chiara; Sharygina, Natasha; Barone-Adesi, Katerina A model checking-based approach for security policy verification of mobile systems. (English) Zbl 1242.68153 Formal Asp. Comput. 23, No. 5, 627-648 (2011). MSC: 68Q60 68N30 PDFBibTeX XMLCite \textit{C. Braghin} et al., Formal Asp. Comput. 23, No. 5, 627--648 (2011; Zbl 1242.68153) Full Text: DOI HAL
Cheney, James; Urban, Christian Mechanizing the metatheory of mini-XQuery. (English) Zbl 1350.68054 Jouannaud, Jean-Pierre (ed.) et al., Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-25378-2/pbk). Lecture Notes in Computer Science 7086, 280-295 (2011). MSC: 68N15 68N18 68T15 PDFBibTeX XMLCite \textit{J. Cheney} and \textit{C. Urban}, Lect. Notes Comput. Sci. 7086, 280--295 (2011; Zbl 1350.68054) Full Text: DOI
Weiß, Benjamin Predicate abstraction in a program logic calculus. (English) Zbl 1221.68066 Sci. Comput. Program. 76, No. 10, 861-876 (2011). MSC: 68N30 68Q60 PDFBibTeX XMLCite \textit{B. Weiß}, Sci. Comput. Program. 76, No. 10, 861--876 (2011; Zbl 1221.68066) Full Text: DOI
Li, Li; Song, XiaoYu; Gu, Ming; Luo, XiangYu Competent predicate abstraction in model checking. (English) Zbl 1214.68137 Sci. China, Inf. Sci. 54, No. 2, 258-267 (2011). MSC: 68N30 PDFBibTeX XMLCite \textit{L. Li} et al., Sci. China, Inf. Sci. 54, No. 2, 258--267 (2011; Zbl 1214.68137) Full Text: DOI Link
Maingaud, Séverine; Balat, Vincent; Bubel, Richard; Hähnle, Reiner; Miquel, Alexandre Specifying imperative ML-like programs using dynamic logic. (English) Zbl 1308.68044 Beckert, Bernhard (ed.) et al., Formal verification of object-oriented software. International conference, FoVeOOS 2010, Paris, France, June 28–30, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-18069-9/pbk). Lecture Notes in Computer Science 6528, 122-137 (2011). MSC: 68N30 03B70 68Q60 PDFBibTeX XMLCite \textit{S. Maingaud} et al., Lect. Notes Comput. Sci. 6528, 122--137 (2011; Zbl 1308.68044) Full Text: DOI
Malecha, Gregory; Morrisett, Greg; Wisnesky, Ryan Trace-based verification of imperative programs with I/O. (English) Zbl 1215.68070 J. Symb. Comput. 46, No. 2, 95-118 (2011). MSC: 68N30 68N01 PDFBibTeX XMLCite \textit{G. Malecha} et al., J. Symb. Comput. 46, No. 2, 95--118 (2011; Zbl 1215.68070) Full Text: DOI
Gast, Holger Reasoning about memory layouts. (English) Zbl 1211.68086 Form. Methods Syst. Des. 37, No. 2-3, 141-170 (2010). MSC: 68N30 03B70 PDFBibTeX XMLCite \textit{H. Gast}, Form. Methods Syst. Des. 37, No. 2--3, 141--170 (2010; Zbl 1211.68086) Full Text: DOI
Rinderknecht, Christian; Volanschi, Nic Theory and practice of unparsed patterns for metacompilation. (English) Zbl 1191.68173 Sci. Comput. Program. 75, No. 3, 85-105 (2010). MSC: 68N20 68P10 PDFBibTeX XMLCite \textit{C. Rinderknecht} and \textit{N. Volanschi}, Sci. Comput. Program. 75, No. 3, 85--105 (2010; Zbl 1191.68173) Full Text: DOI
Tlili, Syrine; Debbabi, Mourad Interprocedural and flow-sensitive type analysis for memory and type safety of C code. (English) Zbl 1192.68125 J. Autom. Reasoning 42, No. 2-4, 265-300 (2009). MSC: 68N15 68N25 PDFBibTeX XMLCite \textit{S. Tlili} and \textit{M. Debbabi}, J. Autom. Reasoning 42, No. 2--4, 265--300 (2009; Zbl 1192.68125) Full Text: DOI
Emmi, Michael; Jhala, Ranjit; Kohler, Eddie; Majumdar, Rupak Verifying reference counting implementations. (English) Zbl 1234.68254 Kowalewski, Stefan (ed.) et al., Tools and algorithms for the construction and analysis of systems. 15th international conference, TACAS 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22–29, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-00767-5/pbk). Lecture Notes in Computer Science 5505, 352-367 (2009). MSC: 68Q60 68N30 PDFBibTeX XMLCite \textit{M. Emmi} et al., Lect. Notes Comput. Sci. 5505, 352--367 (2009; Zbl 1234.68254) Full Text: DOI
Haddad, Serge; Poizat, Pascal Transactional reduction of component compositions. (English) Zbl 1215.68067 Derrick, John (ed.) et al., Formal techniques for networked and distributed systems – FORTE 2007. 27th IFIP WG 6.1 international conference, Tallinn, Estonia, June 27–29, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73195-5/pbk). Lecture Notes in Computer Science 4574, 341-357 (2007). MSC: 68N30 68Q85 PDFBibTeX XMLCite \textit{S. Haddad} and \textit{P. Poizat}, Lect. Notes Comput. Sci. 4574, 341--357 (2007; Zbl 1215.68067) Full Text: DOI
Talpin, Jean-Pierre; Guernic, Paul Le; Shukla, Sandeep Kumar; Gupta, Rajesh A compositional behavioral modeling framework for embedded system design and conformance checking. (English) Zbl 1100.68070 Int. J. Parallel Program. 33, No. 6, 613-643 (2005). MSC: 68Q60 68Q05 PDFBibTeX XMLCite \textit{J.-P. Talpin} et al., Int. J. Parallel Program. 33, No. 6, 613--643 (2005; Zbl 1100.68070) Full Text: DOI HAL