×

Found 591 Documents (Results 1–100)

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

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

Concrete abstractions. Formalizing and analyzing discrete theories and algorithms with the RISCAL model checker. (English) Zbl 1515.68009

Texts & Monographs in Symbolic Computation. Cham: Springer (ISBN 978-3-031-24933-4/hbk; 978-3-031-24936-5/pbk; 978-3-031-24934-1/ebook). xii, 271 p. (2023).
PDFBibTeX XMLCite
Full Text: DOI

Formalization of functional block diagrams using HOL theorem proving. (English) Zbl 07724794

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, 22-35 (2022).
MSC:  68V20 68M15 90B25
PDFBibTeX XMLCite
Full Text: DOI

A framework for substructural type systems. (English) Zbl 07722320

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, 376-402 (2022).
PDFBibTeX XMLCite
Full Text: DOI

Exploring formalisation. A primer in human-readable mathematics in Lean 3 with examples from simplicial topology. (English) Zbl 1496.68006

Surveys and Tutorials in the Applied Mathematical Sciences 11. Cham: Springer (ISBN 978-3-031-14648-0/pbk; 978-3-031-14649-7/ebook). iv, 147 p. (2022).
PDFBibTeX XMLCite
Full Text: DOI

Higher-order logic as a lingua franca for logico-pluralist argumentation. (English) Zbl 1509.68247

Liao, Beishui (ed.) et al., Logics for new-generation AI. Second international workshop, Zhuhai, China, June 10–12, 2022. London: College Publications. 83-94 (2022).
PDFBibTeX XMLCite

Gradability in MTT-semantics. (English) Zbl 07570773

Ö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

Proceedings of the seventeenth international workshop on the ACL2 theorem prover and its applications, Austin, Texas, USA, May 26–27, 2022. (English) Zbl 1489.68031

Electronic Proceedings in Theoretical Computer Science (EPTCS) 359. Waterloo: Open Publishing Association (OPA). 216 p., electronic only, open access (2022).
PDFBibTeX XMLCite
Full Text: DOI Link

A formalization of Dedekind domains and class groups of global fields. (English) Zbl 1523.68167

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 5, 19 p. (2021).
PDFBibTeX XMLCite
Full Text: DOI

Verified quadratic virtual substitution for real arithmetic. (English) Zbl 1521.68246

Huisman, Marieke (ed.) et al., Formal methods. 24th international symposium, FM 2021, virtual event, November 20–26, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13047, 200-217 (2021).
PDFBibTeX XMLCite
Full Text: DOI arXiv

Reasoning about iteration and recursion uniformly based on big-step semantics. (English) Zbl 1498.68077

Qin, Shengchao (ed.) et al., Dependable software engineering. Theories, tools, and applications. 7th international symposium, SETTA 2021, Beijing, China, November 25–27, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13071, 61-80 (2021).
PDFBibTeX XMLCite
Full Text: DOI arXiv

A verified decision procedure for orders in Isabelle/HOL. (English) Zbl 1497.68549

Hou, Zhe (ed.) et al., Automated technology for verification and analysis. 19th international symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12971, 127-143 (2021).
MSC:  68V20 03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

A formal semantics of the GraalVM intermediate representation. (English) Zbl 1497.68104

Hou, Zhe (ed.) et al., Automated technology for verification and analysis. 19th international symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18–22, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12971, 111-126 (2021).
MSC:  68N20 68Q55 68V20
PDFBibTeX XMLCite
Full Text: DOI arXiv

Generating custom set theories with non-set structured objects. (English) Zbl 1485.03221

Kamareddine, Fairouz (ed.) et al., Intelligent computer mathematics. 14th international conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12833, 228-244 (2021).
MSC:  03E70 68V20
PDFBibTeX XMLCite
Full Text: DOI

A new export of the Mizar mathematical library. (English) Zbl 1485.68294

Kamareddine, Fairouz (ed.) et al., Intelligent computer mathematics. 14th international conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12833, 205-210 (2021).
MSC:  68V20 68V30 68V35
PDFBibTeX XMLCite
Full Text: DOI

Formalization of RBD-based cause consequence analysis in HOL. (English) Zbl 1485.68289

Kamareddine, Fairouz (ed.) et al., Intelligent computer mathematics. 14th international conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12833, 47-64 (2021).
MSC:  68V20 68M15 90B25
PDFBibTeX XMLCite
Full Text: DOI

Formalizing axiomatic systems for propositional logic in Isabelle/HOL. (English) Zbl 1485.68292

Kamareddine, Fairouz (ed.) et al., Intelligent computer mathematics. 14th international conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12833, 32-46 (2021).
MSC:  68V20 03B05 03B20
PDFBibTeX XMLCite
Full Text: DOI Link

Beautiful formalizations in Isabelle/Naproche. (English) Zbl 1485.68290

Kamareddine, Fairouz (ed.) et al., Intelligent computer mathematics. 14th international conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12833, 19-31 (2021).
MSC:  68V20
PDFBibTeX XMLCite
Full Text: DOI

A modular first formalisation of combinatorial design theory. (English) Zbl 1485.68291

Kamareddine, Fairouz (ed.) et al., Intelligent computer mathematics. 14th international conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12833, 3-18 (2021).
MSC:  68V20 05Bxx 06D22
PDFBibTeX XMLCite
Full Text: DOI arXiv

Filter Results by …

Document Type

Database

all top 5

Author

all top 5

Serial

all top 5

Year of Publication

all top 3

Main Field