×

Found 78 Documents (Results 1–78)

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

The Braga method: extracting certified algorithms from complex recursive schemes in Coq. (English) Zbl 1528.68392

Mainzer, Klaus (ed.) et al., Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school “Proof and computation”, September 20–26, 2019. Hackensack, NJ: World Scientific. 305-386 (2022).
MSC:  68V15 68N19 68N30
PDFBibTeX XMLCite
Full Text: DOI HAL

Counterexample-guided partial bounding for recursive function synthesis. (English) Zbl 1493.68107

Silva, Alexandra (ed.) et al., Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12759, 832-855 (2021).
MSC:  68N30 68N18
PDFBibTeX XMLCite
Full Text: DOI

Program verification by coinduction. (English) Zbl 1418.68060

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, 589-618 (2018).
MSC:  68N30 68Q55 68Q60 68T15
PDFBibTeX XMLCite
Full Text: DOI

Explicit effect subtyping. (English) Zbl 1418.68065

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, 327-354 (2018).
MSC:  68N30 68N15 68N18
PDFBibTeX XMLCite
Full Text: DOI arXiv

Towards automatic resource bound analysis for OCaml. (English) Zbl 1380.68123

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). 359-373 (2017).
MSC:  68N30 68N15 68N20
PDFBibTeX XMLCite
Full Text: DOI arXiv

Context-free session type inference. (English) Zbl 1485.68072

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, 804-830 (2017).
PDFBibTeX XMLCite
Full Text: DOI HAL

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

Programs using syntax with first-class binders. (English) Zbl 1485.68064

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, 504-529 (2017).
MSC:  68N30 68N15 68N18
PDFBibTeX XMLCite
Full Text: DOI

Set-theoretic types for polymorphic variants. (English) Zbl 1360.68318

Garrigue, Jacques (ed.) et al., Proceedings of the 21st ACM SIGPLAN international conference on functional programming, ICFP ’16, Nara, Japan, September 18–22, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4219-3). 387-391 (2016).
MSC:  68N18 68N30
PDFBibTeX XMLCite
Full Text: DOI arXiv HAL

Partial type equivalences for verified dependent interoperability. (English) Zbl 1360.68322

Garrigue, Jacques (ed.) et al., Proceedings of the 21st ACM SIGPLAN international conference on functional programming, ICFP ’16, Nara, Japan, September 18–22, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4219-3). 298-310 (2016).
MSC:  68N18 68Q60 68T15
PDFBibTeX XMLCite
Full Text: DOI HAL

Chapar: certified causally consistent distributed key-value stores. (English) Zbl 1347.68117

Bodik, Rastislav (ed.) et al., Proceedings of the 43rd annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’16, St. Petersburg, FL, USA, January 20–22, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-3549-2). 357-370 (2016).
MSC:  68P20 68Q55 68Q60 68T15
PDFBibTeX XMLCite
Full Text: DOI

Polyhedral approximation of multivariate polynomials using Handelman’s theorem. (English) Zbl 1475.68093

Jobstmann, Barbara (ed.) et al., Verification, model checking, and abstract interpretation. 17th international conference, VMCAI 2016, St. Petersburg, FL, USA, January 17–19, 2016. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9583, 166-184 (2016).
PDFBibTeX XMLCite
Full Text: DOI HAL

Typeful normalization by evaluation. (English) Zbl 1367.68051

Herbelin, Hugo (ed.) et al., 20th international conference on types for proofs and programs, TYPES’14, Paris, France, May 12–15, 2014. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-88-0). LIPIcs – Leibniz International Proceedings in Informatics 39, 72-88 (2015).
MSC:  68N18 68N30 68Q65
PDFBibTeX XMLCite
Full Text: DOI

1ML – core and modules united (F-ing first-class modules). (English) Zbl 1360.68338

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). 35-47 (2015).
PDFBibTeX XMLCite
Full Text: DOI

Fiat: deductive synthesis of abstract data types in a proof assistant. (English) Zbl 1346.68175

Proceedings of the 42nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’15, Mumbai, India, January 12–18, 2015. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-3300-9). 689-700 (2015).
MSC:  68T15 68N18 68Q60 68Q65
PDFBibTeX XMLCite
Full Text: DOI

A generic intermediate representation for verification condition generation. (English) Zbl 1473.68051

Falaschi, Moreno (ed.), Logic-based program synthesis and transformation. 25th international symposium, LOPSTR 2015, Siena, Italy, July 13–15, 2015. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 9527, 227-243 (2015).
MSC:  68N30 68Q60
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

Lem: reusable engineering of real-world semantics. (English) Zbl 1346.68123

Proceedings of the 19th ACM SIGPLAN international conference on functional programming, ICFP ’14, Gothenburg, Sweden, September 1–3, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2873-9). 175-188 (2014).
MSC:  68Q60 68Q55 68T15
PDFBibTeX XMLCite
Full Text: DOI

Automatic termination verification for higher-order functional programs. (English) Zbl 1347.68231

Shao, Zhong (ed.), Programming languages and systems. 23rd European symposium on programming, ESOP 2014, held as part of the European joint conferences on theory and practice of software, ETAPS 2014, Grenoble, France, April 5–13, 2014. Proceedings. Berlin: Springer (ISBN 978-3-642-54832-1/pbk). Lecture Notes in Computer Science 8410, 392-411 (2014).
MSC:  68Q60 68N18
PDFBibTeX XMLCite
Full Text: DOI

Toward general diagnosis of static errors. (English) Zbl 1284.68141

Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14, San Diego, CA, USA, January 22–24, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2544-8). 569-581 (2014).
PDFBibTeX XMLCite
Full Text: DOI

A trusted mechanised JavaSript specification. (English) Zbl 1284.68381

Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14, San Diego, CA, USA, January 22–24, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2544-8). 87-100 (2014).
MSC:  68Q60 68N30 68T15 68N15
PDFBibTeX XMLCite
Full Text: DOI

Contractive signatures with recursive types, type parameters, and abstract types. (English) Zbl 1335.68057

Fomin, Fedor V. (ed.) et al., Automata, languages, and programming. 40th international colloquium, ICALP 2013, Riga, Latvia, July 8–12, 2013, Proceedings, Part II. Berlin: Springer (ISBN 978-3-642-39211-5/pbk). Lecture Notes in Computer Science 7966, 299-311 (2013).
MSC:  68N30 03B70
PDFBibTeX XMLCite
Full Text: DOI

GADTs meet subtyping. (English) Zbl 1381.68060

Felleisen, Matthias (ed.) et al., Programming languages and systems. 22nd European symposium on programming, ESOP 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16–24, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-37035-9/pbk). Lecture Notes in Computer Science 7792, 554-573 (2013).
MSC:  68N30 68N18 68Q65
PDFBibTeX XMLCite
Full Text: DOI arXiv

Why3 – where programs meet provers. (English) Zbl 1435.68366

Felleisen, Matthias (ed.) et al., Programming languages and systems. 22nd European symposium on programming, ESOP 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16–24, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 7792, 125-128 (2013).
MSC:  68V15 68N30 68Q60
PDFBibTeX XMLCite
Full Text: DOI

Typing unmarshalling without marshalling types. (English) Zbl 1291.68121

Proceedings of the 17th ACM SIGPLAN international conference on functional programming, ICFP ’12, Copenhagen, Denmark, September 9–15, 2012. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-1054-3). ACM SIGPLAN Notices 47, No. 9, 287-298 (2012).
MSC:  68N18 68N15 68Q65
PDFBibTeX XMLCite
Full Text: DOI Link

A certified constraint solver over finite domains. (English) Zbl 1372.68165

Giannakopoulou, Dimitra (ed.) et al., FM 2012: Formal methods. 18th international symposium, Paris, France, August 27–31, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32758-2/pbk). Lecture Notes in Computer Science 7436, 116-131 (2012).
MSC:  68Q60 68T15 68T20
PDFBibTeX XMLCite
Full Text: DOI

A semantic model for graphical user interfaces. (English) Zbl 1323.68129

Proceedings of the 16th ACM SIGPLAN international conference on functional programming, ICFP ’11, Tokyo, Japan, September 19–21, 2011. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-0865-6). ACM SIGPLAN Notices 46, No. 9, 45-57 (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

Automated certification of implicit induction proofs. (English) Zbl 1350.68245

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, 37-53 (2011).
MSC:  68T15 68Q60
PDFBibTeX XMLCite
Full Text: DOI

The first-order nominal link. (English) Zbl 1326.68083

Alpuente, María (ed.), Logic-based program synthesis and transformation. 20th international symposium, LOPSTR 2010, Hagenberg, Austria, July 23–25, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-20550-7/pbk). Lecture Notes in Computer Science 6564, 234-248 (2011).
MSC:  68N30
PDFBibTeX XMLCite
Full Text: DOI

Dependent types from counterexamples. (English) Zbl 1312.68041

Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’10, Madrid, Spain, January 17–23, 2010. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-479-9). 119-130 (2010).
PDFBibTeX XMLCite
Full Text: DOI Link

Extending Coq with imperative features and its application to SAT verification. (English) Zbl 1291.68318

Kaufmann, Matt (ed.) et al., Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14051-8/pbk). Lecture Notes in Computer Science 6172, 83-98 (2010).
MSC:  68T15 68Q60
PDFBibTeX XMLCite
Full Text: DOI Link

Verifying distributed systems: the operational approach. (English) Zbl 1315.68105

Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’09, Savannah, GA, USA, January 18–24, 2009. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-379-2). 429-440 (2009).
MSC:  68N30 68N19 68M14 68Q60 68T15
PDFBibTeX XMLCite
Full Text: DOI

A rewriting logic approach to type inference. (English) Zbl 1253.68211

Corradini, Andrea (ed.) et al., Recent trends in algebraic development techniques. 19th international workshop, WADT 2008, Pisa, Italy, June 13–16, 2008. Revised selected papers. Berlin: Springer (ISBN 978-3-642-03428-2/pbk). Lecture Notes in Computer Science 5486, 135-151 (2009).
MSC:  68Q55 68N30 68Q42
PDFBibTeX XMLCite
Full Text: DOI

Turning inductive into equational specifications. (English) Zbl 1252.68249

Berghofer, Stefan (ed.) et al., Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03358-2/pbk). Lecture Notes in Computer Science 5674, 131-146 (2009).
MSC:  68T15 68N17 68N18 68Q60
PDFBibTeX XMLCite
Full Text: DOI

Implementing real numbers with RZ. (English) Zbl 1262.03076

Dilhage, R. (ed.) et al., Proceedings of the fourth international conference on computability and complexity in analysis (CCA 2007), Siena, Italy, June 16–18, 2007. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 202, 365-384 (2008).
MSC:  03D78 68N30 68Q60
PDFBibTeX XMLCite
Full Text: DOI

On normalization by evaluation for object calculi. (English) Zbl 1138.68350

Miculan, Marino (ed.) et al., Types for proofs and programs. International conference, TYPES 2007, Cividale des Friuli, Italy, May 2–5, 2007. Revised selected papers. Berlin: Springer (ISBN 978-3-540-68084-0/pbk). Lecture Notes in Computer Science 4941, 173-187 (2008).
MSC:  68N18 68N30
PDFBibTeX XMLCite
Full Text: DOI

Lightweight static capabilities. (English) Zbl 1277.68052

Stump, Aron (ed.) et al., Proceedings of the programming languages meets program verification (PLPV 2006), Seattle, WA, USA, August 21, 2006. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 174, No. 7, 79-104 (2007).
MSC:  68N19 68N18 68Q60
PDFBibTeX XMLCite
Full Text: DOI

RZ: A tool for bringing constructive and computable mathematics closer to programming practice. (English) Zbl 1150.03300

Cooper, S. Barry (ed.) et al., Computation and logic in the real world. Third conference on computability in Europe, CiE 2007, Siena, Italy, June 18–23, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73000-2/pbk). Lecture Notes in Computer Science 4497, 28-42 (2007).
PDFBibTeX XMLCite
Full Text: DOI

Static analysis of string manipulations in critical embedded C programs. (English) Zbl 1225.68064

Yi, Kwangkeun (ed.), Static analysis. 13th international symposium, SAS 2006, Seoul, Korea, August 29–31, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-37756-6/pbk). Lecture Notes in Computer Science 4134, 35-51 (2006).
MSC:  68N30 68Q55
PDFBibTeX XMLCite
Full Text: DOI

Verification: industrial applications. (English) Zbl 1129.68447

Schwichtenberg, Helmut (ed.) et al., Proof technology and computation. Papers from the summer school, Marktoberdorf, Germany, July 29–August 10, 2003. Amsterdam: IOS Press (ISBN 1-58603-625-4/hbk). NATO Science Series III: Computer & Systems Sciences 200, 161-205 (2006).
MSC:  68Q60 68T15
PDFBibTeX XMLCite

Verification of an error correcting code by abstract interpretation. (English) Zbl 1111.68507

Cousot, Radhia (ed.), Verfication, model checking, and abstract interpretation. 6th international conference, VMCAI 2005, Paris, France, January 17–19, 2005. Proceedings. Berlin: Springer (ISBN 3-540-24297-X/pbk). Lecture Notes in Computer Science 3385, 330-345 (2005).
MSC:  68Q60 94B15 94B50
PDFBibTeX XMLCite
Full Text: DOI

Extracting a data flow analyser in constructive logic. (English) Zbl 1126.68345

Schmidt, David (ed.), Programming languages and systems. 13th European symposium on programming, ESOP 2004, held as part of the joint European conferences on theory and practice of software, ETAPS 2004, Barcelona, Spain, March 29 – April 2, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21313-9/pbk). Lecture Notes in Computer Science 2986, 385-400 (2004).
MSC:  68N30 03B70
PDFBibTeX XMLCite
Full Text: DOI

Functors for proofs and programs. (English) Zbl 1126.68475

Schmidt, David (ed.), Programming languages and systems. 13th European symposium on programming, ESOP 2004, held as part of the joint European conferences on theory and practice of software, ETAPS 2004, Barcelona, Spain, March 29 – April 2, 2004. Proceedings. Berlin: Springer (ISBN 3-540-21313-9/pbk). Lecture Notes in Computer Science 2986, 370-384 (2004).
MSC:  68Q60 68P05
PDFBibTeX XMLCite
Full Text: DOI

Inferring type isomorphisms generically. (English) Zbl 1106.68337

Kozen, Dexter (ed.), Mathematics of program construction. 7th international conference, MPC 2004, Stirling, Scotland, UK, July 12–14, 2004. Proceedings. Berlin: Springer (ISBN 3-540-22380-0/pbk). Lecture Notes in Computer Science 3125, 32-53 (2004).
MSC:  68N30 68N18
PDFBibTeX XMLCite
Full Text: DOI

A compiled implementation of strong reduction. (English) Zbl 1322.68053

Proceedings of the 7th ACM SIGPLAN international conference on functional programming, ICFP ’02, Pittsburgh, PA, USA, October 4–6, 2002. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-487-8). ACM SIGPLAN Notices 37, No. 9, 235-246 (2002).
MSC:  68N30 68N18 68Q60 68T15
PDFBibTeX XMLCite
Full Text: DOI HAL

Exception analysis for non-strict languages. (English) Zbl 1322.68041

Proceedings of the 7th ACM SIGPLAN international conference on functional programming, ICFP ’02, Pittsburgh, PA, USA, October 4–6, 2002. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-487-8). ACM SIGPLAN Notices 37, No. 9, 98-109 (2002).
PDFBibTeX XMLCite
Full Text: DOI

Automating type soundness proofs via decision procedures and guided reductions. (English) Zbl 1023.68539

Baaz, Matthias (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 9th international conference, LPAR 2002, Tbilisi, Georgia, October 14-18, 2002. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2514, 418-434 (2002).
MSC:  68N30 68T15
PDFBibTeX XMLCite
Full Text: Link

A unifying approach to goal-directed evaluation. (English) Zbl 1030.68542

Taha, Walid (ed.), Semantics, applications, and implementation of program generation. 2nd international workshop, SAIG 2001, Florence, Italy, September 6, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2196, 108-125 (2001).
MSC:  68N30 68N15 68N20
PDFBibTeX XMLCite
Full Text: Link

A calculus for compiling and linking classes. (English) Zbl 0971.68575

Smolka, Gerd (ed.), Programming languages and systems. 9th European symposium on programming, ESOP 2000. Held as part of the joint European conferences on theory and practice of software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1782, 135-149 (2000).
MSC:  68U99 68N15 68N30
PDFBibTeX XMLCite

Filter Results by …

Document Type

all top 5

Author

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software