×

Found 12 Documents (Results 1–12)

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

Witnessing (co)datatypes. (English) Zbl 1335.68224

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, 359-382 (2015).
MSC:  68T15 68Q65
PDFBibTeX XMLCite
Full Text: DOI Link

Cardinals in Isabelle/HOL. (English) Zbl 1416.68152

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, 111-127 (2014).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI Link

MaSh: machine learning for Sledgehammer. (English) Zbl 1317.68215

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, 35-50 (2013).
MSC:  68T15 68T05
PDFBibTeX XMLCite
Full Text: DOI Link

TFF1: the TPTP typed first-order form with rank-1 polymorphism. (English) Zbl 1381.68260

Bonacina, Maria Paola (ed.), Automated deduction – CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9–14, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-38573-5/pbk). Lecture Notes in Computer Science 7898. Lecture Notes in Artificial Intelligence, 414-420 (2013).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI Link

Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. (English) Zbl 1362.68251

Proceedings of the 2012 27th annual ACM/IEEE symposium on logic in computer science, LICS 2012, Dubrovnik, Croatia, June 25–28, 2012. Los Alamitos, CA: IEEE Computer Society (ISBN 978-0-7695-4769-5). 596-605 (2012).
MSC:  68T15 68Q65
PDFBibTeX XMLCite
Full Text: DOI

Extending Sledgehammer with SMT solvers. (English) Zbl 1314.68271

Bjørner, Nikolaj (ed.) et al., Automated deduction – CADE-23. 23rd international conference on automated deduction, Wrocław, Poland, July 31 – August 5, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22437-9/pbk; 978-3-642-22438-6/ebook). Lecture Notes in Computer Science 6803. Lecture Notes in Artificial Intelligence, 116-130 (2011).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI

Filter Results by …

Document Type

all top 5

Year of Publication

Main Field

all top 3

Software