×

Found 43 Documents (Results 1–43)

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
Full Text: DOI

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
Full Text: DOI arXiv

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
Full Text: arXiv Link

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
Full Text: DOI Link

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
Full Text: DOI Link

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
Full Text: DOI

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
Full Text: DOI

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
Full Text: DOI

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
Full Text: DOI

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
Full Text: DOI

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).
PDFBibTeX XMLCite
Full Text: DOI HAL

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
Full Text: DOI

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).
PDFBibTeX XMLCite
Full Text: DOI arXiv Link

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
Full Text: DOI

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
Full Text: DOI

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
Full Text: DOI

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
Full Text: DOI

Filter Results by …

Document Type

all top 5

Author

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software