×

Found 41 Documents (Results 1–41)

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

\( \pi\) with leftovers: a mechanisation in Agda. (English) Zbl 1490.68143

Peters, Kirstin (ed.) et al., Formal techniques for distributed objects, components, and systems. 41st IFIP WG 6.1 international conference, FORTE 2021, held as part of the 16th international federated conference on distributed computing techniques, DisCoTec 2021, Valletta, Malta, June 14–18, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12719, 157-174 (2021).
PDFBibTeX XMLCite
Full Text: DOI arXiv

Is impredicativity implicitly implicit? (English) Zbl 07756114

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:  03B70 68N30
PDFBibTeX XMLCite
Full Text: DOI

Type theory unchained: extending Agda with user-defined rewrite rules. (English) Zbl 07756107

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 2, 27 p. (2020).
MSC:  03B70 68N30
PDFBibTeX XMLCite
Full Text: DOI

Galois connections for recursive types. (English) Zbl 1440.68042

Di Pierro, Alessandra (ed.) et al., From lambda calculus to cybersecurity through program analysis. Essays dedicated to Chris Hankin on the occasion of his retirement. Cham: Springer. Lect. Notes Comput. Sci. 12065, 105-131 (2020).
PDFBibTeX XMLCite
Full Text: DOI

A flexible categorial formalisation of term graphs as directed hypergraphs. (English) Zbl 1444.68053

Fiadeiro, José Luiz (ed.) et al., Recent trends in algebraic development techniques. 24th IFIP WG 1.3 international workshop, WADT 2018, Egham, UK, July 2–5, 2018. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 11563, 103-118 (2019).
PDFBibTeX XMLCite
Full Text: DOI

PML2: integrated program verification in ML. (English) Zbl 1528.68083

Abel, Andreas (ed.) et al., 23rd international conference on types for proofs and programs, TYPES 2017, May 24 – June 1, 2017, Budapest, Hungary. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 104, Article 4, 27 p. (2018).
MSC:  68N30 03B70 68N18
PDFBibTeX XMLCite
Full Text: DOI arXiv

A formal equational theory for call-by-push-value. (English) Zbl 1511.68086

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, 523-541 (2018).
MSC:  68N30 68N18
PDFBibTeX XMLCite
Full Text: DOI

Synthesis of recursive ADT transformations from reusable templates. (English) Zbl 1452.68050

Legay, Axel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Part I. Berlin: Springer. Lect. Notes Comput. Sci. 10205, 247-263 (2017).
MSC:  68N30
PDFBibTeX XMLCite
Full Text: DOI arXiv Link

Automatically generating the dynamic semantics of gradually typed languages. (English) Zbl 1380.68082

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). 789-803 (2017).
MSC:  68N15 68N17 68N30
PDFBibTeX XMLCite
Full Text: DOI

Hazelnut: a bidirectionally typed structure editor calculus. (English) Zbl 1380.68100

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). 86-99 (2017).
MSC:  68N18 68N30
PDFBibTeX XMLCite
Full Text: DOI arXiv

Automatically proving equivalence by type-safe reflection. (English) Zbl 1367.68257

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, 40-55 (2017).
MSC:  68T15 68N30
PDFBibTeX XMLCite
Full Text: DOI Link

Unifiers as equivalences: proof-relevant unification of dependently typed data. (English) Zbl 1360.68321

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). 270-283 (2016).
MSC:  68N18 68N30
PDFBibTeX XMLCite
Full Text: DOI Link

A classical realizability model for a semantical value restriction. (English) Zbl 1335.68059

Thiemann, Peter (ed.), Programming languages and systems. 25th European symposium on programming, ESOP 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-49497-4/pbk; 978-3-662-49498-1/ebook). Lecture Notes in Computer Science 9632, 476-502 (2016).
MSC:  68N30
PDFBibTeX XMLCite
Full Text: DOI arXiv

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

Mathematics of program construction. 12th international conference, MPC 2015, Königswinter, Germany, June 29 – July 1, 2015. Proceedings. (English) Zbl 1312.68008

Lecture Notes in Computer Science 9129. Cham: Springer (ISBN 978-3-319-19796-8/pbk; 978-3-319-19797-5/ebook). xiv, 323 p. (2015).
MSC:  68-06 68N30 00B25
PDFBibTeX XMLCite
Full Text: DOI

Overlapping and order-independent patterns. Definitional equality for all. (English) Zbl 1405.68075

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, 87-106 (2014).
MSC:  68N30 68N15 68Q55
PDFBibTeX XMLCite
Full Text: DOI

Combining proofs and programs in a dependently typed language. (English) Zbl 1284.68125

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). 33-45 (2014).
PDFBibTeX XMLCite
Full Text: DOI Link

Extracting a DPLL algorithm. (English) Zbl 1342.68293

Berger, Ulrich (ed.) et al., Proceedings of the 28th conference on the mathematical foundations of programming semantics (MFPS XXVIII), Bath, UK, June 6–9, 2012. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 286, 243-256 (2012).
MSC:  68T15 68N30
PDFBibTeX XMLCite
Full Text: DOI

Self-certification: bootstrapping certified typecheckers in F\(^\ast\) with Coq. (English) Zbl 1321.68205

Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’12, Philadelphia, PA, USA, January 22–28, 2012. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-1083-3). 571-584 (2012).
MSC:  68N30 68N15 68N19 68T15
PDFBibTeX XMLCite
Full Text: DOI

The lax braided structure of streaming I/O. (English) Zbl 1247.68088

Bezem, Marc (ed.), Computer science logic (CSL’11). 25th international workshop, 20th annual conference of the EACSL, Bergen, Norway, September 12–15, 2011. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-32-3). LIPIcs – Leibniz International Proceedings in Informatics 12, 292-306, electronic only (2011).
MSC:  68Q05 18B20 18D10 68N18 68N30 68T15
PDFBibTeX XMLCite
Full Text: DOI Link

Irrelevance in type theory with a heterogeneous equality judgement. (English) Zbl 1326.68076

Hofmann, Martin (ed.), Foundations of software science and computational structures. 14th international conference, FOSSACS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19804-5/pbk). Lecture Notes in Computer Science 6604, 57-71 (2011).
MSC:  68N30
PDFBibTeX XMLCite
Full Text: DOI

Program calculation in Coq. (English) Zbl 1308.68049

Johnson, Michael (ed.) et al., Algebraic methodology and software technology. 13th international conference, AMAST 2010, Lac-Beauport, QC, Canada, June 23–25, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-17795-8/pbk). Lecture Notes in Computer Science 6486, 163-179 (2011).
MSC:  68N30 68T15
PDFBibTeX XMLCite
Full Text: DOI

Dependent types and program equivalence. (English) Zbl 1312.68062

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). 275-286 (2010).
MSC:  68N30 68N15
PDFBibTeX XMLCite
Full Text: DOI Link

Security-typed programming within dependently typed programming. (English) Zbl 1323.68220

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, 169-180 (2010).
MSC:  68N30 68N15 68Q60
PDFBibTeX XMLCite
Full Text: DOI

Subtyping, declaratively. An exercise in mixed induction and coinduction. (English) Zbl 1286.68074

Bolduc, Claude (ed.) et al., Mathematics of program construction. 10th international conference, MPC 2010, Québec City, Canada, June 21–23, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-13320-6/pbk). Lecture Notes in Computer Science 6120, 100-118 (2010).
MSC:  68N30
PDFBibTeX XMLCite
Full Text: DOI

Dependently typed grammars. (English) Zbl 1286.68259

Bolduc, Claude (ed.) et al., Mathematics of program construction. 10th international conference, MPC 2010, Québec City, Canada, June 21–23, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-13320-6/pbk). Lecture Notes in Computer Science 6120, 58-79 (2010).
MSC:  68Q42 68N30
PDFBibTeX XMLCite
Full Text: DOI

Verifying a semantic \(\beta \eta \)-conversion test for Martin-Löf type theory. (English) Zbl 1157.68025

Audebaud, Philippe (ed.) et al., Mathematics of program construction. 9th international conference, MPC 2008, Marseille, France, July 15–18, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-70593-2/pbk). Lecture Notes in Computer Science 5133, 29-56 (2008).
MSC:  68N30 68N18 68T15
PDFBibTeX XMLCite
Full Text: DOI

Interfaces as games, programs as strategies. (English) Zbl 1172.68423

Filliâtre, Jean-Christophe (ed.) et al., Types for proofs and programs. International workshop, TYPES 2004, Jouy-en-Josas, France, December 15–18, 2004. Revised selected papers. Berlin: Springer (ISBN 3-540-31428-8/pbk). Lecture Notes in Computer Science 3839, 215-231 (2006).
MSC:  68N30 03B15 68T15 91A40
PDFBibTeX XMLCite
Full Text: DOI

State dependent IO-monads in type theory. (English) Zbl 1272.68106

Birkedal, L. (ed.), Proceedings of the 10th conference on category theory in computer science (CTCS 2004), Copenhagen, Denmark, August 12–14, 2004. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 122, 127-146 (2005).
PDFBibTeX XMLCite
Full Text: Link

Implementing algebraic dynamic programming in the functional and the imperative programming paradigm. (English) Zbl 1073.68574

Boiten, Eerke A. (ed.) et al., Mathematics of program construction. 6th international conference, MPC 2002, Dagstuhl Castle, Germany, July 8–10, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43857-2). Lect. Notes Comput. Sci. 2386, 1-20 (2002).
MSC:  68N30 68N18 90C39
PDFBibTeX XMLCite
Full Text: Link

Filter Results by …

Document Type

all top 5

Author

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software