{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T01:05:22Z","timestamp":1725584722557},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642210693"},{"type":"electronic","value":"9783642210709"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21070-9_18","type":"book-chapter","created":{"date-parts":[[2011,6,7]],"date-time":"2011-06-07T04:02:27Z","timestamp":1307419347000},"page":"230-247","source":"Crossref","is-referenced-by-count":5,"title":["Dependently-Typed Formalisation of Relation-Algebraic Abstractions"],"prefix":"10.1007","author":[{"given":"Wolfram","family":"Kahl","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"8","key":"18_CR1","doi-asserted-by":"publisher","first-page":"1126","DOI":"10.1109\/TC.2008.223","volume":"58","author":"C.K. Anand","year":"2009","unstructured":"Anand, C.K., Kahl, W.: An optimized Cell BE special function library generated by Coconut. IEEE Transactions on Computers\u00a058(8), 1126\u20131138 (2009)","journal-title":"IEEE Transactions on Computers"},{"issue":"2","key":"18_CR2","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1017\/S0956796802004501","volume":"13","author":"G. Barthe","year":"2003","unstructured":"Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Program.\u00a013(2), 261\u2013293 (2003)","journal-title":"J. Funct. Program."},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Relations and Kleene Algebra in Computer Science","year":"2009","unstructured":"Berghammer, R., Jaoua, A.M., M\u00f6ller, B. (eds.): RelMiCS 2009. LNCS, vol.\u00a05827. Springer, Heidelberg (2009)"},{"key":"18_CR4","series-title":"International Series in Computer Science","volume-title":"Algebra of Programming","author":"R.S. Bird","year":"1997","unstructured":"Bird, R.S., de Moor, O.: Algebra of Programming. International Series in Computer Science, vol.\u00a0100. Prentice-Hall, Englewood Cliffs (1997)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/3-540-48256-3_10","volume-title":"Theorem Proving in Higher Order Logics","author":"V. Capretta","year":"1999","unstructured":"Capretta, V.: Universal algebra in type theory. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 131\u2013148. Springer, Heidelberg (1999)"},{"key":"18_CR6","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1142\/9789812384720_0003","volume-title":"Handbook of Graph Grammars and Computing by Graph Transformation, Foundations","author":"A. Corradini","year":"1997","unstructured":"Corradini, A., Montanari, U., Rossi, F., Ehrig, H., Heckel, R., L\u00f6we, M.: Algebraic approaches to graph transformation, part I: Basic concepts and double pushout approach. In: Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation, Foundations, vol.\u00a01, ch. 3, pp. 163\u2013245. World Scientific, Singapore (1997)"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Jipsen, P., Struth, G.: Domain and antidomain semigroups. In: Berghammer et al. [3], pp. 73\u201387","DOI":"10.1007\/978-3-642-04639-1_6"},{"key":"18_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/S0020-0255(01)00168-2","volume":"139","author":"J. Desharnais","year":"2001","unstructured":"Desharnais, J., M\u00f6ller, B.: Characterizing determinacy in Kleene algebras. Information Sciences\u00a0139, 253\u2013273 (2001)","journal-title":"Information Sciences"},{"issue":"4","key":"18_CR9","doi-asserted-by":"publisher","first-page":"798","DOI":"10.1145\/1183278.1183285","volume":"7","author":"J. Desharnais","year":"2006","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Kleene algebra with domain. ACM Transactions on Computational Logic\u00a07(4), 798\u2013833 (2006)","journal-title":"ACM Transactions on Computational Logic"},{"key":"18_CR10","volume-title":"Categories, Allegories, North-Holland Mathematical Library","author":"P.J. Freyd","year":"1990","unstructured":"Freyd, P.J., Scedrov, A.: Categories, Allegories. North-Holland Mathematical Library, vol.\u00a039. North-Holland, Amsterdam (1990)"},{"key":"18_CR11","unstructured":"Furusawa, H., Kahl, W.: A study on symmetric quotients. Tech. Rep. 1998-06, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t der Bundeswehr M\u00fcnchen (December 1998)"},{"key":"18_CR12","unstructured":"Gonzal\u00eda, C.: Relations in Dependent Type Theory. Ph.D. thesis, also as Technical Report No.\u00a014D, Department of Computer Science and Engineering, Chalmers University of Technology, G\u00f6teborg University (2006)"},{"key":"18_CR13","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1142\/9789812794499_0021","volume-title":"Current Trends in Theoretical Computer Science","author":"Y. Gurevich","year":"1993","unstructured":"Gurevich, Y.: Evolving Algebras: An attempt to discover semantics. In: Rozenberg, G., Salomaa, A. (eds.) Current Trends in Theoretical Computer Science, pp. 266\u2013292. World Scientific, Singapore (1993)"},{"issue":"1","key":"18_CR14","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/343369.343384","volume":"1","author":"Y. Gurevich","year":"2000","unstructured":"Gurevich, Y.: Sequential abstract state machines capture sequential algorithms. ACM Transactions on Computational Logic\u00a01(1), 77\u2013111 (2000)","journal-title":"ACM Transactions on Computational Logic"},{"key":"18_CR15","unstructured":"Han, J.: Proofs of Relational Semigroupoids in Isabelle\/Isar. M.Sc.\u00a0thesis, McMaster University, Department of Computing and Software (2008)"},{"key":"18_CR16","series-title":"Foundations Of Computing Series","doi-asserted-by":"crossref","first-page":"239","DOI":"10.7551\/mitpress\/5641.003.0015","volume-title":"Proof, language, and interaction: Essays in honour of Robin Milner","author":"G. Huet","year":"2000","unstructured":"Huet, G., Sa\u00efbi, A.: Constructive category theory. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, language, and interaction: Essays in honour of Robin Milner. Foundations of Computing Series, pp. 239\u2013275. MIT Press, Cambridge (2000)"},{"key":"18_CR17","unstructured":"Jackson, P.B.: Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra. Ph.D. thesis, Cornell University (1995)"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-24771-5_16","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"W. Kahl","year":"2004","unstructured":"Kahl, W.: Calculational relation-algebraic proofs in Isabelle\/Isar. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol.\u00a03051, pp. 178\u2013190. Springer, Heidelberg (2004)"},{"issue":"1","key":"18_CR19","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/j.jlap.2007.10.008","volume":"76","author":"W. Kahl","year":"2008","unstructured":"Kahl, W.: Relational semigroupoids: Abstract relation-algebraic interfaces for finite relations between infinite types. J. Logic and Algebraic Programming\u00a076(1), 60\u201389 (2008)","journal-title":"J. Logic and Algebraic Programming"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Kahl, W.: Collagories for relational adhesive rewriting. In: Berghammer et al [3], pp. 211\u2013226","DOI":"10.1007\/978-3-642-04639-1_15"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-642-15928-2_24","volume-title":"Graph Transformations","author":"W. Kahl","year":"2010","unstructured":"Kahl, W.: Amalgamating pushout and pullback graph transformation in collagories. In: Ehrig, H., Rensink, A., Rozenberg, G., Sch\u00fcrr, A. (eds.) ICGT 2010. LNCS, vol.\u00a06372, pp. 362\u2013378. Springer, Heidelberg (2010)"},{"key":"18_CR22","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1016\/j.jlap.2010.07.017","volume":"79","author":"W. Kahl","year":"2010","unstructured":"Kahl, W.: Determinisation of relational substitutions in ordered categories with domain. J. Logic and Algebraic Programming\u00a079, 812\u2013829 (2010)","journal-title":"J. Logic and Algebraic Programming"},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1007\/3-540-10856-4_125","volume-title":"Mathematical Foundations of Computer Science 1981","author":"A. Kanda","year":"1981","unstructured":"Kanda, A.: Constructive category theory (no.\u00a01). In: Gruska, J., Chytil, M.P. (eds.) MFCS 1981. LNCS, vol.\u00a0118, pp. 563\u2013577. Springer, Heidelberg (1981)"},{"key":"18_CR24","unstructured":"McCune, W.: Prover9 and Mace4, version LADR-2009-11A (2009), http:\/\/www.prover9.org\/"},{"key":"18_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-70594-9_15","volume-title":"Mathematics of Program Construction","author":"S.C. Mu","year":"2008","unstructured":"Mu, S.C., Ko, H.S., Jansson, P.: Algebra of programming using dependent types. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol.\u00a05133, pp. 268\u2013283. Springer, Heidelberg (2008)"},{"key":"18_CR26","unstructured":"Norell, U.: Towards a Practical Programming Language Based on Dependent Type Theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology (September 2007)"},{"key":"18_CR27","series-title":"Advances in Computing Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-7091-6510-2_3","volume-title":"Relational Methods in Computer Science","author":"G. Schmidt","year":"1997","unstructured":"Schmidt, G., Hattensperger, C., Winter, M.: Heterogeneous relation algebra. In: Brink, C., Kahl, W., Schmidt, G. (eds.) Relational Methods in Computer Science. Advances in Computing Science, ch.\u00a03, pp. 39\u201353. Springer, Wien (1997)"},{"key":"18_CR28","volume-title":"EATCS-Monographs on Theoret. Comput. Sci.","author":"G. Schmidt","year":"1993","unstructured":"Schmidt, G., Str\u00f6hlein, T.: Relations and Graphs, Discrete Mathematics for Computer Scientists. EATCS-Monographs on Theoret. Comput. Sci. Springer, Heidelberg (1993)"},{"key":"18_CR29","unstructured":"West, S., Kahl, W.: A generic graph transformation, visualisation, and editing framework in Haskell. In: Boronat, A., Heckel, R. (eds.) Proceedings of the Eighth International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT 2009). Electronic Communications of the EASST, vol.\u00a018, pp. 12.1\u201312.18 (September 2009)"}],"container-title":["Lecture Notes in Computer Science","Relational and Algebraic Methods in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21070-9_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,7]],"date-time":"2024-04-07T10:20:44Z","timestamp":1712485244000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21070-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642210693","9783642210709"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21070-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}