Saito, Ayumu; Affeldt, Reynald 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 \textit{A. Saito} and \textit{R. Affeldt}, Lect. Notes Comput. Sci. 13544, 151--177 (2022; Zbl 07705361) Full Text: DOI
Xie, Ruifeng; Hu, Zhenjiang Generic recursive lens combinators and their calculation laws. (English) Zbl 1499.68071 Theor. Comput. Sci. 913, 113-137 (2022). MSC: 68N30 68N15 PDFBibTeX XMLCite \textit{R. Xie} and \textit{Z. Hu}, Theor. Comput. Sci. 913, 113--137 (2022; Zbl 1499.68071) Full Text: DOI
Zalakain, Uma; Dardha, Ornela \( \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). MSC: 68Q85 03B70 68N30 68Q60 68V20 PDFBibTeX XMLCite \textit{U. Zalakain} and \textit{O. Dardha}, Lect. Notes Comput. Sci. 12719, 157--174 (2021; Zbl 1490.68143) Full Text: DOI arXiv
Monnier, Stefan; Bos, Nathaniel 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 \textit{S. Monnier} and \textit{N. Bos}, LIPIcs -- Leibniz Int. Proc. Inform. 175, Article 9, 19 p. (2020; Zbl 07756114) Full Text: DOI
Cockx, Jesper 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 \textit{J. Cockx}, LIPIcs -- Leibniz Int. Proc. Inform. 175, Article 2, 27 p. (2020; Zbl 07756107) Full Text: DOI
Al-Sibahi, Ahmad Salim; Jensen, Thomas; Møgelberg, Rasmus Ejlers; Wąsowski, Andrzej 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). MSC: 68N18 06A15 68N15 68N30 68Q42 PDFBibTeX XMLCite \textit{A. S. Al-Sibahi} et al., Lect. Notes Comput. Sci. 12065, 105--131 (2020; Zbl 1440.68042) Full Text: DOI
Cohen, Liron; Faro, Sofia Abreu; Tate, Ross The effects of effects on constructivism. (English) Zbl 07515956 König, Barbara (ed.), Proceedings of the 35th conference on the mathematical foundations of programming semantics, MFPS XXXV, London, UK, June 4–7, 2019. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 347, 87-120 (2019). MSC: 68N30 68Q55 PDFBibTeX XMLCite \textit{L. Cohen} et al., Electron. Notes Theor. Comput. Sci. 347, 87--120 (2019; Zbl 07515956) Full Text: DOI
Kahl, Wolfram; Zhao, Yuhang 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). MSC: 68N30 05C65 68P05 68Q42 PDFBibTeX XMLCite \textit{W. Kahl} and \textit{Y. Zhao}, Lect. Notes Comput. Sci. 11563, 103--118 (2019; Zbl 1444.68053) Full Text: DOI
Lepigre, Rodolphe 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 \textit{R. Lepigre}, LIPIcs -- Leibniz Int. Proc. Inform. 104, Article 4, 27 p. (2018; Zbl 1528.68083) Full Text: DOI arXiv
Rizkallah, Christine; Garbuzov, Dmitri; Zdancewic, Steve 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 \textit{C. Rizkallah} et al., Lect. Notes Comput. Sci. 10895, 523--541 (2018; Zbl 1511.68086) Full Text: DOI
Stump, Aaron From realizability to induction via dependent intersection. (English) Zbl 1469.03037 Ann. Pure Appl. Logic 169, No. 7, 637-655 (2018). MSC: 03B38 03B40 68N18 68N30 PDFBibTeX XMLCite \textit{A. Stump}, Ann. Pure Appl. Logic 169, No. 7, 637--655 (2018; Zbl 1469.03037) Full Text: DOI
Kocsis, Zoltan A.; Swan, Jerry Genetic programming \(+\) proof search \(=\) automatic improvement. (English) Zbl 1425.68076 J. Autom. Reasoning 60, No. 2, 157-176 (2018). MSC: 68N30 68T20 PDFBibTeX XMLCite \textit{Z. A. Kocsis} and \textit{J. Swan}, J. Autom. Reasoning 60, No. 2, 157--176 (2018; Zbl 1425.68076) Full Text: DOI
Inala, Jeevana Priya; Polikarpova, Nadia; Qiu, Xiaokang; Lerner, Benjamin S.; Solar-Lezama, Armando 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 \textit{J. P. Inala} et al., Lect. Notes Comput. Sci. 10205, 247--263 (2017; Zbl 1452.68050) Full Text: DOI arXiv Link
Uustalu, Tarmo; Veltri, Niccolò Finiteness and rational sequences, constructively. (English) Zbl 1418.68069 J. Funct. Program. 27, Paper No. e13, 20 p. (2017). MSC: 68N30 03F50 PDFBibTeX XMLCite \textit{T. Uustalu} and \textit{N. Veltri}, J. Funct. Program. 27, Paper No. e13, 20 p. (2017; Zbl 1418.68069) Full Text: DOI
Cimini, Matteo; Siek, Jeremy G. 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 \textit{M. Cimini} and \textit{J. G. Siek}, in: 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). 789--803 (2017; Zbl 1380.68082) Full Text: DOI
Omar, Cyrus; Voysey, Ian; Hilton, Michael; Aldrich, Jonathan; Hammer, Matthew A. 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 \textit{C. Omar} et al., in: 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). 86--99 (2017; Zbl 1380.68100) Full Text: DOI arXiv
Slama, Franck; Brady, Edwin 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 \textit{F. Slama} and \textit{E. Brady}, Lect. Notes Comput. Sci. 10383, 40--55 (2017; Zbl 1367.68257) Full Text: DOI Link
Cockx, Jesper; Devriese, Dominique; Piessens, Frank 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 \textit{J. Cockx} et al., in: 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). 270--283 (2016; Zbl 1360.68321) Full Text: DOI Link
Chiang, Yu-Hsi; Mu, Shin-Cheng Formal derivation of greedy algorithms from relational specifications: a tutorial. (English) Zbl 1355.68049 J. Log. Algebr. Methods Program. 85, No. 5, Part 2, 879-905 (2016). MSC: 68N30 68N15 68T15 PDFBibTeX XMLCite \textit{Y.-H. Chiang} and \textit{S.-C. Mu}, J. Log. Algebr. Methods Program. 85, No. 5, Part 2, 879--905 (2016; Zbl 1355.68049) Full Text: DOI
Lepigre, Rodolphe 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 \textit{R. Lepigre}, Lect. Notes Comput. Sci. 9632, 476--502 (2016; Zbl 1335.68059) Full Text: DOI arXiv
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy 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 \textit{J. C. Blanchette} et al., in: 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). 192--204 (2015; Zbl 1360.68358) Full Text: DOI arXiv Link
Hinze, Ralf (ed.); Voigtländer, Janis (ed.) 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 \textit{R. Hinze} (ed.) and \textit{J. Voigtländer} (ed.), Mathematics of program construction. 12th international conference, MPC 2015, Königswinter, Germany, June 29 -- July 1, 2015. Proceedings. Cham: Springer (2015; Zbl 1312.68008) Full Text: DOI
Cockx, Jesper; Piessens, Frank; Devriese, Dominique 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 \textit{J. Cockx} et al., Lect. Notes Comput. Sci. 8410, 87--106 (2014; Zbl 1405.68075) Full Text: DOI
Casinghino, Chris; Sjöberg, Vilhelm; Weirich, Stephanie 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). MSC: 68N18 68Q60 68N30 68Q55 03B40 03B70 PDFBibTeX XMLCite \textit{C. Casinghino} et al., in: 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). 33--45 (2014; Zbl 1284.68125) Full Text: DOI Link
Lawrence, Andrew; Berger, Ulrich; Seisenberger, Monika 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 \textit{A. Lawrence} et al., Electron. Notes Theor. Comput. Sci. 286, 243--256 (2012; Zbl 1342.68293) Full Text: DOI
Strub, Pierre-Yves; Swamy, Nikhil; Fournet, Cedric; Chen, Juan 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 \textit{P.-Y. Strub} et al., in: 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). 571--584 (2012; Zbl 1321.68205) Full Text: DOI
Abel, Andreas; Scherer, Gabriel On irrelevance and algorithmic equality in predicative type theory. (English) Zbl 1238.03028 Log. Methods Comput. Sci. 8, No. 1, Paper No. 29, 36 p. (2012). MSC: 03B70 68N30 PDFBibTeX XMLCite \textit{A. Abel} and \textit{G. Scherer}, Log. Methods Comput. Sci. 8, No. 1, Paper No. 29, 36 p. (2012; Zbl 1238.03028) Full Text: DOI arXiv
Jeffrey, Alan; Rathke, Julian 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 \textit{A. Jeffrey} and \textit{J. Rathke}, LIPIcs -- Leibniz Int. Proc. Inform. 12, 292--306 (2011; Zbl 1247.68088) Full Text: DOI Link
Abel, Andreas 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 \textit{A. Abel}, Lect. Notes Comput. Sci. 6604, 57--71 (2011; Zbl 1326.68076) Full Text: DOI
Tesson, Julien; Hashimoto, Hideki; Hu, Zhenjiang; Loulergue, Frédéric; Takeichi, Masato 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 \textit{J. Tesson} et al., Lect. Notes Comput. Sci. 6486, 163--179 (2011; Zbl 1308.68049) Full Text: DOI
Jia, Limin; Zhao, Jianzhou; Sjöberg, Vilhelm; Weirich, Stephanie 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 \textit{L. Jia} et al., in: 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). 275--286 (2010; Zbl 1312.68062) Full Text: DOI Link
Morgenstern, Jamie; Licata, Daniel R. 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 \textit{J. Morgenstern} and \textit{D. R. Licata}, in: 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). 169--180 (2010; Zbl 1323.68220) Full Text: DOI
Boute, Raymond Pointfree expression and calculation: From quantification to temporal logic. (English) Zbl 1211.68080 Form. Methods Syst. Des. 37, No. 2-3, 95-140 (2010). MSC: 68N30 68Q60 03B70 PDFBibTeX XMLCite \textit{R. Boute}, Form. Methods Syst. Des. 37, No. 2--3, 95--140 (2010; Zbl 1211.68080) Full Text: DOI
Danielsson, Nils Anders; Altenkirch, Thorsten 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 \textit{N. A. Danielsson} and \textit{T. Altenkirch}, Lect. Notes Comput. Sci. 6120, 100--118 (2010; Zbl 1286.68074) Full Text: DOI
Brink, Kasper; Holdermans, Stefan; Löh, Andres 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 \textit{K. Brink} et al., Lect. Notes Comput. Sci. 6120, 58--79 (2010; Zbl 1286.68259) Full Text: DOI
Abel, Andreas; Coquand, Thierry; Dybjer, Peter 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 \textit{A. Abel} et al., Lect. Notes Comput. Sci. 5133, 29--56 (2008; Zbl 1157.68025) Full Text: DOI
Michelbrink, Markus 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 \textit{M. Michelbrink}, Lect. Notes Comput. Sci. 3839, 215--231 (2006; Zbl 1172.68423) Full Text: DOI
Michelbrink, Markus Interfaces as functors, programs as coalgebras – a final coalgebra theorem in intensional type theory. (English) Zbl 1099.03020 Theor. Comput. Sci. 360, No. 1-3, 415-439 (2006). MSC: 03B70 03G30 68N30 03F35 18D15 68Q65 68Q85 PDFBibTeX XMLCite \textit{M. Michelbrink}, Theor. Comput. Sci. 360, No. 1--3, 415--439 (2006; Zbl 1099.03020) Full Text: DOI
Dybjer, Peter; Setzer, Anton Indexed induction-recursion. (English) Zbl 1080.68014 J. Log. Algebr. Program. 66, No. 1, 1-49 (2006). MSC: 68N30 03B70 03D70 PDFBibTeX XMLCite \textit{P. Dybjer} and \textit{A. Setzer}, J. Log. Algebr. Program. 66, No. 1, 1--49 (2006; Zbl 1080.68014) Full Text: DOI
Michelbrink, Markus; Setzer, Anton 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). MSC: 68N30 03F35 18C15 68Q65 PDFBibTeX XMLCite \textit{M. Michelbrink} and \textit{A. Setzer}, Electron. Notes Theor. Comput. Sci. 122, 127--146 (2005; Zbl 1272.68106) Full Text: Link
Giegerich, Robert; Steffen, Peter 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 \textit{R. Giegerich} and \textit{P. Steffen}, Lect. Notes Comput. Sci. 2386, 1--20 (2002; Zbl 1073.68574) Full Text: Link