×

Found 727 Documents (Results 1–100)

A Coq formalization of Lebesgue induction principle and Tonelli’s theorem. (English) Zbl 1529.68315

Chechik, Marsha (ed.) et al., Formal methods. 25th international symposium, FM 2023, Lübeck, Germany, March 6–10, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14000, 39-55 (2023).
PDFBibTeX XMLCite
Full Text: DOI HAL

LibNDT: Towards a formal library on spreadable properties over linked nested datatypes. (English) Zbl 07779291

Gibbons, Jeremy (ed.) et al., Proceedings of the ninth workshop on mathematically structured functional programming, MSFP 2022, Munich, Germany, April 2, 2022. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 360, 27-44 (2022).
MSC:  68-XX 06-XX
PDFBibTeX XMLCite
Full Text: arXiv Link

A sound strategy to compile general recursion into finite depth pattern matching. (English) Zbl 1528.68050

Lima, Lucas (ed.) et al., Formal methods: foundations and applications. 25th Brazilian symposium, SBMF 2022, virtual event, December 6–9, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13768, 39-54 (2022).
MSC:  68N15 68N18
PDFBibTeX XMLCite
Full Text: DOI

Integration of multiple formal matrix models in Coq. (English) Zbl 1528.68396

Dong, Wei (ed.) et al., Dependable software engineering. Theories, tools, and applications. 8th international symposium, SETTA 2022, Beijing, China, October 27–29, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13649, 169-186 (2022).
MSC:  68V20
PDFBibTeX XMLCite
Full Text: DOI

Region-based resource management and lexical exception handlers in continuation-passing style. (English) Zbl 1528.68052

Sergey, Ilya (ed.), Programming languages and systems. 31st European symposium on programming, ESOP 2022, held as part of the European joint conferences on theory and practice of software, ETAPS 2022, Munich, Germany, April 2–7, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13240, 492-519 (2022).
MSC:  68N15 68N18
PDFBibTeX XMLCite
Full Text: DOI

Towards a practical library for monadic equational reasoning in Coq. (English) Zbl 07705361

Komendantskaya, Ekaterina (ed.), Mathematics of program construction. 14th international conference, MPC 2022, Tbilisi, Georgia, September 26–28, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13544, 151-177 (2022).
MSC:  68N30
PDFBibTeX XMLCite
Full Text: DOI

Experiments with automated reasoning in the class. (English) Zbl 07691306

Buzzard, Kevin (ed.) et al., Intelligent computer mathematics. 15th international conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13467, 287-304 (2022).
MSC:  68Vxx
PDFBibTeX XMLCite
Full Text: DOI HAL

An integrated web platform for the Mizar Mathematical Library. (English) Zbl 07691295

Buzzard, Kevin (ed.) et al., Intelligent computer mathematics. 15th international conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13467, 141-146 (2022).
MSC:  68Vxx
PDFBibTeX XMLCite
Full Text: DOI arXiv

Automating the functional correspondence between higher-order evaluators and abstract machines. (English) Zbl 1521.68033

De Angelis, Emanuele (ed.) et al., Logic-based program synthesis and transformation. 31st international symposium, LOPSTR 2021, Tallinn, Estonia, September 7–8, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13290, 38-59 (2022).
MSC:  68N30 68N20
PDFBibTeX XMLCite
Full Text: DOI arXiv

Verified erasure correction in Coq with MathComp and VST. (English) Zbl 1514.68071

Shoham, Sharon (ed.) et al., Computer aided verification. 34th international conference, CAV 2022, Haifa, Israel, August 7–10, 2022. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 13372, 272-292 (2022).
MSC:  68P30 68V15
PDFBibTeX XMLCite
Full Text: DOI

Certified verification of relational properties. (English) Zbl 1502.68077

ter Beek, Maurice H. (ed.) et al., Integrated formal methods. 17th international conference, IFM 2022, Lugano, Switzerland, June 7–10, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13274, 86-105 (2022).
MSC:  68N30 68Q60
PDFBibTeX XMLCite
Full Text: DOI arXiv Link

Gradability in MTT-semantics. (English) Zbl 1530.03120

Özgün, Aybüke (ed.) et al., Language, logic, and computation. 13th International Tbilisi symposium, TbiLLC 2019, Batumi, Georgia, September 16–20, 2019. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 13206, 38-59 (2022).
MSC:  03B65 03B38 68V20
PDFBibTeX XMLCite
Full Text: DOI

Translation certification for smart contracts. (English) Zbl 07570116

Hanus, Michael (ed.) et al., Functional and logic programming. 16th international symposium, FLOPS 2022, Kyoto, Japan, May 10–12, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13215, 94-111 (2022).
MSC:  68N17 68N18
PDFBibTeX XMLCite
Full Text: DOI arXiv

Generalized arrays for Stainless frames. (English) Zbl 1498.68172

Finkbeiner, Bernd (ed.) et al., Verification, model checking, and abstract interpretation. 23rd international conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13182, 332-354 (2022).
PDFBibTeX XMLCite
Full Text: DOI Link

Verifying an HTTP key-value server with interaction trees and VST. (English) Zbl 07699449

Cohen, Liron (ed.) et al., 12th international conference on interactive theorem proving, ITP 2021, Rome, Italy, virtual conference, June 29 – July 1, 2021. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 193, Article 32, 19 p. (2021).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI

Verifying the conversion into CNF in Dafny. (English) Zbl 07547739

Silva, Alexandra (ed.) et al., Logic, language, information, and computation. 27th international workshop, WoLLIC 2021, virtual event, October 5–8, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13038, 150-166 (2021).
MSC:  68V15 03B35
PDFBibTeX XMLCite
Full Text: DOI

A mechanically verified theory of contracts. (English) Zbl 07500642

Cerone, Antonio (ed.) et al., Theoretical aspects of computing – ICTAC 2021. 18th international colloquium, virtual event, Nur-Sultan, Kazakhstan, September 8–10, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12819, 134-151 (2021).
MSC:  68Qxx
PDFBibTeX XMLCite
Full Text: DOI arXiv

Functional correctness of C implementations of Dijkstra’s, Kruskal’s, and Prim’s algorithms. (English) Zbl 1493.68216

Silva, Alexandra (ed.) et al., Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12760, 801-826 (2021).
MSC:  68Q60 68R10 68V15
PDFBibTeX XMLCite
Full Text: DOI

Harpoon: mechanizing metatheory interactively. (English) Zbl 07437106

Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 636-648 (2021).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI

Deductive verification of floating-point Java programs in KeY. (English) Zbl 1474.68186

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 242-261 (2021).
MSC:  68Q60 65G50 68N15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Verified software units. (English) Zbl 1473.68035

Yoshida, Nobuko (ed.), Programming languages and systems. 30th European symposium on programming, ESOP 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12648, 118-147 (2021).
PDFBibTeX XMLCite
Full Text: DOI

Is impredicativity implicitly implicit? (English) Zbl 1535.03067

Bezem, Marc (ed.) et al., 25th international conference on types for proofs and programs. TYPES 2019, June 11–14, 2019, Oslo, Norway. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 175, Article 9, 19 p. (2020).
MSC:  03B40 68N18
PDFBibTeX XMLCite
Full Text: DOI

\(\eta\)-equivalence in core dependent Haskell. (English) Zbl 1535.68044

Bezem, Marc (ed.) et al., 25th international conference on types for proofs and programs. TYPES 2019, June 11–14, 2019, Oslo, Norway. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 175, Article 7, 31 p. (2020).
MSC:  68N18
PDFBibTeX XMLCite
Full Text: DOI

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

Trakhtenbrot’s theorem in Coq. A constructive approach to finite model theory. (English) Zbl 07614663

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, 79-96 (2020).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Competing inheritance paths in dependent type theory: a case study in functional analysis. (English) Zbl 07614659

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, 3-20 (2020).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI

Semantic foundations for deterministic dataflow and stream processing. (English) Zbl 1508.68069

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, 394-427 (2020).
MSC:  68N30 68Q10 68Q55
PDFBibTeX XMLCite
Full Text: DOI

A formalization of properties of continuous functions on closed intervals. (English) Zbl 1503.68298

Bigatti, Anna Maria (ed.) et al., Mathematical software – ICMS 2020. 7th international conference, Braunschweig, Germany, July 13–16, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12097, 272-280 (2020).
PDFBibTeX XMLCite
Full Text: DOI

A proof assistant based formalisation of a subset of sequential core Erlang. (English) Zbl 1475.68059

Byrski, Aleksander (ed.) et al., Trends in functional programming. 21st international symposium, TFP 2020, Krakow, Poland, February 13–14, 2020. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 12222, 139-158 (2020).
PDFBibTeX XMLCite
Full Text: DOI arXiv Link

Formal adventures in convex and conical spaces. (English) Zbl 1455.68254

Benzmüller, Christoph (ed.) et al., Intelligent computer mathematics. 13th international conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12236, 23-38 (2020).
MSC:  68V20 52A01
PDFBibTeX XMLCite
Full Text: DOI arXiv

Formal verifications of call-by-need and call-by-name evaluations with mutual recursion. (English) Zbl 07834971

Lin, Anthony Widjaja (ed.), Programming languages and systems. 17th Asian symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1–4, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11893, 181-201 (2019).
PDFBibTeX XMLCite
Full Text: DOI

Squeezing streams and composition of self-stabilizing algorithms. (English) Zbl 1533.68398

Pérez, Jorge A. (ed.) et al., Formal techniques for distributed objects, components, and systems. 39th IFIP WG 6.1 international conference, FORTE 2019, held as part of the 14th international federated conference on distributed computing techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17–21, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11535, 21-38 (2019).
MSC:  68W15 68V15
PDFBibTeX XMLCite
Full Text: DOI HAL

Filter Results by …

Document Type

all top 5

Author

all top 5

Serial

all top 5

Year of Publication

all top 3

Main Field

Biographic Reference

all top 3

Software