×

Found 138 Documents (Results 1–100)

LibNDT: Towards a formal library on spreadable properties over linked nested datatypes. (English) Zbl 07779291

Gibbons, Jeremy (ed.) et al., Proceedings of the ninth workshop on mathematically structured functional programming, MSFP 2022, Munich, Germany, April 2, 2022. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 360, 27-44 (2022).
MSC:  68-XX 06-XX
PDFBibTeX XMLCite
Full Text: arXiv Link

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

Big step normalisation for type theory. (English) Zbl 07756109

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 4, 20 p. (2020).
MSC:  68N18 03B40
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

Verifying selective CPS transformation for shift and reset. (English) Zbl 1503.68037

Bowman, William J. (ed.) et al., Trends in functional programming. 20th international symposium, TFP 2019, Vancouver, BC, Canada, June 12–14, 2019. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 12053, 38-57 (2020).
MSC:  68N18 68V20
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 Link

Guarded recursion in Agda via sized types. (English) Zbl 1528.68071

Geuvers, Herman (ed.), 4th international conference on formal structures for computation and deduction, FSCD 2019, Dortmund, Germany, June 24–30, 2019. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 131, Article 32, 19 p. (2019).
MSC:  68N18
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 HAL

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

The sequent calculus of skew monoidal categories. (English) Zbl 1523.18017

Staton, Sam (ed.), Proceedings of the 34th conference on the mathematical foundations of programming semantics (MFPS XXXIV), Dalhousie University, Halifax, Canada, June 6–9, 2018. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 341, 345-370 (2018).
PDFBibTeX XMLCite
Full Text: DOI

Formalizing constructive quantifier elimination in Agda. (English) Zbl 1525.68197

Atkey, Robert (ed.) et al., Proceedings of the 7th workshop on mathematically structured functional programming, MSFP 2018, Oxford, UK, July 8, 2018. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 275, 2-17 (2018).
MSC:  68V20 03B35 03C10
PDFBibTeX XMLCite
Full Text: arXiv Link

A syntax for higher inductive-inductive types. (English) Zbl 1462.68022

Kirchner, Hélène (ed.), 3rd international conference on formal structures for computation and deduction, FSCD 2018, July 9–12, 2018, Oxford, United Kingdom. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 108, Article 20, 18 p. (2018).
MSC:  68N18 03B38 55U35
PDFBibTeX XMLCite
Full Text: DOI

Formalization of universal algebra in Agda. (English) Zbl 1433.68578

Alves, Sandra (ed.) et al., Selected papers of the 12th workshop on logical and semantic frameworks, with applications (LSFA 2017), Brasilia, Brazil, September 23–24, 2017. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 338, 147-166 (2018).
MSC:  68V20 03C05 68V15
PDFBibTeX XMLCite
Full Text: DOI

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

Verified timing transformations in synchronous circuits with \(\lambda\pi\)-Ware. (English) Zbl 1511.68023

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, 504-522 (2018).
PDFBibTeX XMLCite
Full Text: DOI

\(\Pi\)-Ware: hardware description and verification in Agda. (English) Zbl 1433.68081

Uustalu, Tarmo (ed.), 21st international conference on types for proofs and programs, TYPES 2015, May 18–21, 2015, Tallinn, Estonia. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 69, Article 9, 27 p. (2018).
MSC:  68N15 68N18 94C11
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

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

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

Variations on Noetherianness. (English) Zbl 1477.68070

Atkey, Robert (ed.) et al., Proceedings of the sixth workshop on mathematically structured functional programming, MSFP 2016, Eindhoven, Netherlands, April 8, 2016. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 207, 76-88 (2016).
MSC:  68N18 03F65
PDFBibTeX XMLCite
Full Text: arXiv Link

Functions-as-constructors higher-order unification. (English) Zbl 1387.03008

Kesner, Delia (ed.) et al., 1st international conference on formal structures for computation and deduction, FSCD 2016, Porto, Portugal, June 22–26, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-010-1). LIPIcs – Leibniz International Proceedings in Informatics 52, Article 26, 17 p. (2016).
MSC:  03B35 68Q42 68T15
PDFBibTeX XMLCite
Full Text: DOI

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 mechanized textbook proof of a type unification algorithm. (English) Zbl 1335.68236

Cornélio, Márcio (ed.) et al., Formal methods: foundations and applications. 18th Brazilian symposium, SBMF 2015, Belo Horizonte, Brazil, September 21–22, 2015. Proceedings. Cham: Springer (ISBN 978-3-319-29472-8/pbk; 978-3-319-29473-5/ebook). Lecture Notes in Computer Science 9526, 127-141 (2016).
MSC:  68T15 68N15 68N18
PDFBibTeX XMLCite
Full Text: DOI

Functions out of higher truncations. (English) Zbl 1373.03011

Kreutzer, Stephan (ed.), 24th EACSL annual conference and 29th workshop on computer science logic, CSL’15, Berlin, Germany, September 7–10, 2015. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-90-3). LIPIcs – Leibniz International Proceedings in Informatics 41, 359-373 (2015).
MSC:  03B15 03G30 55U40 68T15
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

A unification algorithm for Coq featuring universe polymorphism and overloading. (English) Zbl 1360.68774

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). 179-191 (2015).
MSC:  68T15 68N18 68T20
PDFBibTeX XMLCite
Full Text: DOI

Auto in Agda. Programming proof search using reflection. (English) Zbl 1432.68063

Hinze, Ralf (ed.) et al., Mathematics of program construction. 12th international conference, MPC 2015, Königswinter, Germany, June 29 – July 1, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9129, 276-301 (2015).
MSC:  68N18 68V15
PDFBibTeX XMLCite
Full Text: DOI

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

Coherence for skew-monoidal categories. (English) Zbl 1464.18018

Levy, Paul (ed.) et al., Proceedings of the fifth workshop on mathematically structured functional programming, MSFP 2014, Grenoble, France, April 12, 2014. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 153, 68-77 (2014).
MSC:  18M50 68Q42 68V20
PDFBibTeX XMLCite
Full Text: arXiv Link

Normalization by evaluation in the delay monad: a case study for coinduction via copatterns and sized types. (English) Zbl 1464.68050

Levy, Paul (ed.) et al., Proceedings of the fifth workshop on mathematically structured functional programming, MSFP 2014, Grenoble, France, April 12, 2014. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 153, 51-67 (2014).
MSC:  68N18 18C15 68V15
PDFBibTeX XMLCite
Full Text: arXiv Link

A type theory for productive coprogramming via guarded recursion. (English) Zbl 1394.68066

Proceedings of the joint meeting of the twenty-third EACSL annual conference on computer science logic, CSL, and the 2014 29th annual ACM/IEEE symposium on logic in computer science, LICS 2014, Vienna, Austria, July 14–18, 2014. Los Alamitos, CA: IEEE Computer Society (ISBN 978-1-4503-2886-9). Paper No. 71, 10 p. (2014).
PDFBibTeX XMLCite
Full Text: DOI

Pattern matching without K. (English) Zbl 1345.68045

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). 257-268 (2014).
MSC:  68N18 03B15 03G30 55U40
PDFBibTeX XMLCite
Full Text: DOI Link

J-Calc: a typed lambda calculus for intuitionistic justification logic. (English) Zbl 1337.03023

de Paiva, Valeria (ed.) et al., Proceedings of the 6th workshop on intuitionistic modal logic and applications (IMLA 2013) in association with UNILOG 2013, Rio de Janeiro, Brazil, April 7, 2013. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 300, 71-87 (2014).
PDFBibTeX XMLCite
Full Text: DOI

A formalized proof of strong normalization for guarded recursive types. (English) Zbl 1453.68035

Garrigue, Jacques (ed.), Programming languages and systems. 12th Asian symposium, APLAS 2014, Singapore, Singapore, November 17–19, 2014, Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8858, 140-158 (2014).
MSC:  68N18 03B70
PDFBibTeX XMLCite
Full Text: DOI

Categories of coalgebras with monadic homomorphisms. (English) Zbl 1445.68119

Bonsangue, M. (ed.), Coalgebraic methods in computer science. 12th IFIP WG 1.3 international workshop, CMCS 2014, colocated with ETAPS 2014, Grenoble, France, April 5–6, 2014. Revised selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 8446, 151-167 (2014).
PDFBibTeX XMLCite
Full Text: DOI HAL

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

Productive coprogramming with guarded recursion. (English) Zbl 1323.68092

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, 197-208 (2013).
MSC:  68N18
PDFBibTeX XMLCite
Full Text: DOI Link

Wellfounded recursion with copatterns: a unified approach to termination and productivity. (English) Zbl 1323.68087

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, 185-196 (2013).
MSC:  68N18 03B70 68P05
PDFBibTeX XMLCite
Full Text: DOI

Typed syntactic meta-programming. (English) Zbl 1323.68109

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, 73-86 (2013).
MSC:  68N18
PDFBibTeX XMLCite
Full Text: DOI Link

Certified parsing of regular languages. (English) Zbl 1303.68077

Gonthier, Georges (ed.) et al., Certified programs and proofs. Third international conference, CPP 2013, Melbourne, VIC, Australia, December 11–13, 2013. Proceedings. Berlin: Springer (ISBN 978-3-319-03544-4/pbk). Lecture Notes in Computer Science 8307, 98-113 (2013).
MSC:  68Q45
PDFBibTeX XMLCite
Full Text: DOI

Copatterns, programming infinite structures by observations. (English) Zbl 1301.68080

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). 27-38 (2013).
MSC:  68N18 68N15
PDFBibTeX XMLCite
Full Text: DOI

A constructive model of uniform continuity. (English) Zbl 1433.03155

Hasegawa, Masahito (ed.), Typed lambda calculi and applications. 11th international conference, TLCA 2013, Eindhoven, The Netherlands, June 26–28, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 7941, 236-249 (2013).
PDFBibTeX XMLCite
Full Text: DOI

Generalizations of Hedberg’s theorem. (English) Zbl 1433.03032

Hasegawa, Masahito (ed.), Typed lambda calculi and applications. 11th international conference, TLCA 2013, Eindhoven, The Netherlands, June 26–28, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 7941, 173-188 (2013).
MSC:  03B38 55U40 68V15
PDFBibTeX XMLCite
Full Text: DOI

Operational semantics using the partiality monad. (English) Zbl 1291.68114

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, 127-138 (2012).
MSC:  68N18
PDFBibTeX XMLCite
Full Text: DOI

Generic programming with dependent types. (English) Zbl 1374.68107

Gibbons, Jeremy (ed.), Generic and indexed programming. International spring school, SSGIP 2010, Oxford, UK, March 22–26, 2010. Revised lectures. Berlin: Springer (ISBN 978-3-642-32201-3/pbk). Lecture Notes in Computer Science 7470, 217-258 (2012).
MSC:  68N19
PDFBibTeX XMLCite
Full Text: DOI

Towards certifiable implementation of graph transformation via relation categories. (English) Zbl 1364.68309

Kahl, Wolfram (ed.) et al., Relational and algebraic methods in computer science. 13th international conference, RAMiCS 2012, Cambridge, UK, September 17–20, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-33313-2/pbk). Lecture Notes in Computer Science 7560, 82-97 (2012).
PDFBibTeX XMLCite
Full Text: DOI

Dependently typed programming based on automated theorem proving. (English) Zbl 1358.68056

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, 220-240 (2012).
MSC:  68N18 68T15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Filter Results by …

Document Type

all top 5

Author

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software