×

Found 182 Documents (Results 1–100)

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

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

Higher-order Tarski Grothendieck as a foundation for formal proof. (English) Zbl 07649958

Harrison, John (ed.) et al., 10th international conference on interactive theorem proving, ITP 2019, September 9–12, 2019, Portland, OR, USA. Proceedings. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 141, Article 9, 16 p. (2019).
MSC:  68V20
PDFBibTeX XMLCite
Full Text: DOI

Into the infinite – theory exploration for coinduction. (English) Zbl 1515.68343

Fleuriot, Jacques (ed.) et al., Artificial intelligence and symbolic computation. 13th international conference, AISC 2018, Suzhou, China, September 16–19, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11110, 70-86 (2018).
MSC:  68V15 68V20
PDFBibTeX XMLCite
Full Text: DOI

Efficient verification of imperative programs using auto2. (English) Zbl 1423.68295

Beyer, Dirk (ed.) et al., Tools and algorithms for the construction and analysis of systems. 24th international conference, TACAS 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 10805, 23-40 (2018).
MSC:  68Q60 68P05 68T15
PDFBibTeX XMLCite
Full Text: DOI arXiv

A verified compiler from Isabelle/HOL to CakeML. (English) Zbl 1418.68045

Ahmed, Amal (ed.), Programming languages and systems. 27th European symposium on programming, ESOP 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10801, 999-1026 (2018).
MSC:  68N20 68N18 68T15
PDFBibTeX XMLCite
Full Text: DOI

Verifying asymptotic time complexity of imperative programs in Isabelle. (English) Zbl 1511.68334

Galmiche, Didier (ed.) et al., Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10900, 532-548 (2018).
MSC:  68V15 68N30 68Q60
PDFBibTeX XMLCite
Full Text: DOI arXiv

Program verification in the presence of cached address translation. (English) Zbl 1468.68069

Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 542-559 (2018).
PDFBibTeX XMLCite
Full Text: DOI

How to simulate it in Isabelle: towards formal proof for secure multi-party computation. (English) Zbl 1483.68486

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, 114-130 (2017).
PDFBibTeX XMLCite
Full Text: DOI arXiv

Beginner’s Luck: a language for property-based generators. (English) Zbl 1380.68096

Castagna, Giuseppe (ed.) et al., Proceedings of the 44th annual ACM SIGPLAN symposium on principles of programming languages, POPL ’17, Paris, France, January 15–21, 2017. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4660-3). 114-129 (2017).
MSC:  68N18
PDFBibTeX XMLCite
Full Text: DOI arXiv

A verified algorithm enumerating event structures. (English) Zbl 1367.68245

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, 239-254 (2017).
MSC:  68T15 05A15 06-04 68Q10 68U35
PDFBibTeX XMLCite
Full Text: DOI arXiv Link

Friends with benefits. Implementing corecursion in foundational proof assistants. (English) Zbl 1485.68280

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, 111-140 (2017).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI

Towards a UTP semantics for Modelica. (English) Zbl 1483.68053

Bowen, Jonathan P. (ed.) et al., Unifying theories of programming. 6th international symposium, UTP 2016, Reykjavik, Iceland, June 4–5, 2016. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 10134, 44-64 (2017).
PDFBibTeX XMLCite
Full Text: DOI Link

Towards compositional feedback in non-deterministic and non-input-receptive systems. (English) Zbl 1401.68013

Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5–8, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4391-6). 768-777 (2016).
MSC:  68M07 68Q10 68Q55 68Q60 68T15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Canonical HybridLF: extending Hybrid with dependent types. (English) Zbl 1394.68351

Benevides, Mario (ed.) et al., Proceedings of the 10th workshop on logical and semantic frameworks, with applications (LSFA 2015), Natal, Brazil, August 31 – September 1, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 323, 125-142 (2016).
MSC:  68T15 03B35 03B40
PDFBibTeX XMLCite
Full Text: DOI

A realizability interpretation for intersection and union types. (English) Zbl 1485.03030

Igarashi, Atsushi (ed.), Programming languages and systems. 14th Asian symposium, APLAS 2016, Hanoi, Vietnam, November 21–23, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10017, 187-205 (2016).
MSC:  03B40
PDFBibTeX XMLCite
Full Text: DOI HAL

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

Equational reasoning with applicative functors. (English) Zbl 1464.68063

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, 252-273 (2016).
MSC:  68N18 18A99 68V15
PDFBibTeX XMLCite
Full Text: DOI

An Isabelle/HOL formalisation of Green’s theorem. (English) Zbl 1468.68312

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, 3-19 (2016).
MSC:  68V20 26B20
PDFBibTeX XMLCite
Full Text: DOI Link

Translating Scala programs to Isabelle/HOL. System description. (English) Zbl 1475.68437

Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9706, 568-577 (2016).
MSC:  68V15 68Q60
PDFBibTeX XMLCite
Full Text: DOI arXiv

A verified SAT solver framework with learn, forget, restart, and incrementality. (English) Zbl 1475.68432

Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9706, 25-44 (2016).
MSC:  68V15 68T05 68T20
PDFBibTeX XMLCite
Full Text: DOI HAL

Foundational extensible corecursion: a proof assistant perspective. (English) Zbl 1360.68358

Proceedings of the 20th ACM SIGPLAN international conference on functional programming, ICFP ’15, Vancouver, Canada, September 1–3, 2015. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-3669-7). 192-204 (2015).
MSC:  68N30 68T15
PDFBibTeX XMLCite
Full Text: DOI arXiv Link

A verified compiler for probability density functions. (English) Zbl 1335.68037

Vitek, Jan (ed.), Programming languages and systems. 24th European symposium on programming, ESOP 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings. Berlin: Springer (ISBN 978-3-662-46668-1/pbk; 978-3-662-46669-8/ebook). Lecture Notes in Computer Science 9032, 80-104 (2015).
MSC:  68N20 68T15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Stream fusion for Isabelle’s code generator. Rough diamond. (English) Zbl 1465.68292

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, 270-277 (2015).
MSC:  68V15 68P05
PDFBibTeX XMLCite
Full Text: DOI

Proof-producing reflection for HOL. With an application to model polymorphism. (English) Zbl 1465.03052

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, 170-186 (2015).
PDFBibTeX XMLCite
Full Text: DOI

Automated theorem proving for special functions: the next phase. (English) Zbl 1346.68176

Watt, Stephen M. (ed.) et al., Proceedings of the 2014 symposium on symbolic-numeric computation, SNC 2014, Shanghai, China, July 28–31, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2963-7). 3-8 (2014).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI

Asynchronous user interaction and tool integration in Isabelle/PIDE. (English) Zbl 1416.68182

Klein, Gerwin (ed.) et al., 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. Berlin: Springer. Lect. Notes Comput. Sci. 8558, 515-530 (2014).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI

Truly modular (co)datatypes for Isabelle/HOL. (English) Zbl 1416.68151

Klein, Gerwin (ed.) et al., 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. Berlin: Springer. Lect. Notes Comput. Sci. 8558, 93-110 (2014).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI Link

Flexary operators for formalized mathematics. (English) Zbl 1304.68171

Watt, Stephen M. (ed.) et al., Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-08433-6/pbk). Lecture Notes in Computer Science 8543. Lecture Notes in Artificial Intelligence, 312-327 (2014).
MSC:  68T30
PDFBibTeX XMLCite
Full Text: DOI

Set theory or higher order logic to represent auction concepts in Isabelle? (English) Zbl 1304.68152

Watt, Stephen M. (ed.) et al., Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-08433-6/pbk). Lecture Notes in Computer Science 8543. Lecture Notes in Artificial Intelligence, 236-251 (2014).
MSC:  68T15 68T30 91B26
PDFBibTeX XMLCite
Full Text: DOI arXiv

Hipster: integrating theory exploration in a proof assistant. (English) Zbl 1304.68157

Watt, Stephen M. (ed.) et al., Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Berlin: Springer (ISBN 978-3-319-08433-6/pbk). Lecture Notes in Computer Science 8543. Lecture Notes in Artificial Intelligence, 108-122 (2014).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Verified decision procedures for MSO on words based on derivatives of regular expressions. (English) Zbl 1323.68346

Proceedings of the 18th ACM SIGPLAN international conference on functional programming, ICFP ’13, Boston, MA, USA, September 25–27, 2013. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2326-0). ACM SIGPLAN Notices 48, No. 9, 3-12 (2013).
MSC:  68Q45 03B25 03D05 68N18 68T15
PDFBibTeX XMLCite
Full Text: DOI Link

The power of parameterization in coinductive proof. (English) Zbl 1301.68220

Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’13, Rome, Italy, January 23–25, 2013. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-1832-7). 193-206 (2013).
MSC:  68T15 06B99 68N18 68N30
PDFBibTeX XMLCite
Full Text: DOI

A parallelized theorem prover for a logic with parallel execution. (English) Zbl 1317.68230

Blazy, Sandrine (ed.) et al., Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39633-5/pbk). Lecture Notes in Computer Science 7998, 435-450 (2013).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI

The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof. (English) Zbl 1383.68071

Hawblitzel, Chris (ed.) et al., Certified programs and proofs. Second international conference, CPP 2012, Kyoto, Japan, December 13–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-35307-9/pbk). Lecture Notes in Computer Science 7679, 92-108 (2012).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI

Using locales to define a rely-guarantee temporal logic. (English) Zbl 1360.68795

Beringer, Lennart (ed.) et al., Interactive theorem proving. Third international conference, ITP 2012, Princeton, NJ, USA, August 13–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32346-1/pbk). Lecture Notes in Computer Science 7406, 299-314 (2012).
MSC:  68T27 03B44 68T15 68T42
PDFBibTeX XMLCite
Full Text: DOI

Unifying correctness statements. (English) Zbl 1358.68100

Gibbons, Jeremy (ed.) et al., Mathematics of program construction. 11th international conference, MPC 2012, Madrid, Spain, June 25–27, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31112-3/pbk). Lecture Notes in Computer Science 7342, 198-219 (2012).
MSC:  68Q05 68Q55 68Q60 68T15
PDFBibTeX XMLCite
Full Text: DOI

Combining interactive and automatic reasoning in first order theories of functional programs. (English) Zbl 1352.68038

Birkedal, Lars (ed.), Foundations of software science and computational structures. 15th international conference, FOSSACS 2012, held as part of the European joint conferences on theory and practice of software, ETAPS 2012, Tallinn, Estonia, March 24 – April 1, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28728-2/pbk). Lecture Notes in Computer Science 7213, 104-118 (2012).
MSC:  68N18 68Q60
PDFBibTeX XMLCite
Full Text: DOI

Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers. (English) Zbl 1352.68159

Bjørner, Nikolaj (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28716-9/pbk). Lecture Notes in Computer Science 7180, 289-303 (2012).
MSC:  68Q60 03B44 68T15
PDFBibTeX XMLCite
Full Text: DOI HAL

Smart testing of functional programs in Isabelle. (English) Zbl 1352.68039

Bjørner, Nikolaj (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, Mérida, Venezuela, March 11–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28716-9/pbk). Lecture Notes in Computer Science 7180, 153-167 (2012).
MSC:  68N18 68T15
PDFBibTeX XMLCite
Full Text: DOI

A theoretical framework for the higher-order cooperation of numeric constraint domains. (English) Zbl 1347.68059

Haeusler, Edward Hermann (ed.) et al., Proceedings of the 5th workshop on logical and semantic frameworks, with applications (LSFA 2010), Natal, Brazil, August 31, 2010. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 269, 55-69 (2011).
PDFBibTeX XMLCite
Full Text: DOI

Smart test data generators via logic programming. (English) Zbl 1245.68168

Gallagher, John P. (ed.) et al., Technical communications of the 27th international conference on logic programming (ICLP 2011), Lexington, Kentucky, USA, July 6–10, 2011. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-31-6). LIPIcs – Leibniz International Proceedings in Informatics 11, 139-150, electronic only (2011).
MSC:  68T15 68N30 68N17 68N18
PDFBibTeX XMLCite
Full Text: DOI Link

Exploring the foundations of discrete analytical geometry in Isabelle/HOL. (English) Zbl 1350.68232

Schreck, Pascal (ed.) et al., Automated deduction in geometry. 8th international workshop, ADG 2010, Munich, Germany, July 22–24, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-25069-9/pbk). Lecture Notes in Computer Science 6877. Lecture Notes in Artificial Intelligence, 34-50 (2011).
MSC:  68T15 03H05 51N99
PDFBibTeX XMLCite
Full Text: DOI

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

Verified efficient enumeration of plane graphs modulo isomorphism. (English) Zbl 1342.68298

Van Eekelen, Marko (ed.) et al., Interactive theorem proving. Second international conference, ITP 2011, Berg en Dal, The Netherlands, August 22–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22862-9/pbk). Lecture Notes in Computer Science 6898, 281-296 (2011).
MSC:  68T15 05B40 05C30 05C60 52C17
PDFBibTeX XMLCite
Full Text: DOI

Validating QBF validity in HOL4. (English) Zbl 1342.68290

Van Eekelen, Marko (ed.) et al., Interactive theorem proving. Second international conference, ITP 2011, Berg en Dal, The Netherlands, August 22–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22862-9/pbk). Lecture Notes in Computer Science 6898, 168-183 (2011).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI

Termination of Isabelle functions via termination of rewriting. (English) Zbl 1342.68289

Van Eekelen, Marko (ed.) et al., Interactive theorem proving. Second international conference, ITP 2011, Berg en Dal, The Netherlands, August 22–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22862-9/pbk). Lecture Notes in Computer Science 6898, 152-167 (2011).
MSC:  68T15 68Q42
PDFBibTeX XMLCite
Full Text: DOI

Logical formalisation and analysis of the Mifare Classic card in PVS. (English) Zbl 1342.68288

Van Eekelen, Marko (ed.) et al., Interactive theorem proving. Second international conference, ITP 2011, Berg en Dal, The Netherlands, August 22–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22862-9/pbk). Lecture Notes in Computer Science 6898, 3-17 (2011).
MSC:  68T15 94A60 94A62
PDFBibTeX XMLCite
Full Text: DOI Link

VeriML: typed computation of logical terms inside a language with effects. (English) Zbl 1323.68384

Proceedings of the 15th ACM SIGPLAN international conference on functional programming, ICFP ’10, Baltimore, MD, USA, September 27–29, 2010. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-794-3). ACM SIGPLAN Notices 45, No. 9, 333-344 (2010).
MSC:  68Q60 68N18 68T15
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