{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:15:34Z","timestamp":1725455734310},"publisher-location":"Berlin, Heidelberg","reference-count":112,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540605898"},{"type":"electronic","value":"9783540478027"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0015460","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T06:32:11Z","timestamp":1131863531000},"page":"148-172","source":"Crossref","is-referenced-by-count":1,"title":["KORSO reference languages concepts and application domains"],"prefix":"10.1007","author":[{"given":"H. -D.","family":"Ehrich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"R.J.R. Back, Refinement Calculus, Part II: Parallel and Reactive Programs, in: [BRR89] 67\u201393.","DOI":"10.1007\/3-540-52559-9_61"},{"key":"8_CR2","unstructured":"J.W. de Bakker, Ed., Languages for Parallel Architectures \u2014 Design, Semantics, Implementation Aspects (Wiley & Sons, 1989)."},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"F.L. Bauer, R. Berghammer, M. Broy, W. Dosch, F. Geiselbrechtinger, R. Gnatz, E. Hangel, W. Hesse, and Krieg-Br\u00fcckner. The Munich Project CIP, Vol 1: The Wide Spectrum Language CIP-L., volume 183 of L.N.C.S. Springer, 1985.","DOI":"10.1007\/3-540-15187-7"},{"key":"8_CR4","first-page":"246","volume-title":"LNCS 186","author":"M. Bidoit","year":"1985","unstructured":"M. Bidoit and C. Choppy. ASSPEGIQUE: An Integrated Environment for Algebraic Specifications. Proc. 1st Int. Joint Conference on Theory and Practice of Software Development (TAPSOFT'85), pages 246\u2013260. LNCS 186, Springer-Verlag, Berlin, 1985."},{"key":"8_CR5","volume-title":"Forschungsberichte des Fachbereichs Informatik 93-30","author":"R. Betschko","year":"1993","unstructured":"Ralph Betschko, Sabine Dick, Klaus Didrich, and Wolfgang Grieskamp. Formal Development of an Efficient Implementation of a Lexical Scanner within the KorSo Methodology Framework. Forschungsberichte des Fachbereichs Informatik 93-30, Technische Universit\u00e4t Berlin, Franklinstra\u00dfe 28\/29-D-10587 Berlin, October 1993."},{"key":"8_CR6","series-title":"Technical Report TUM-I9311","volume-title":"The Requirement and Design Specification Language SPECTRUM. An Informal Introduction. Version 1.0. Part i","author":"M. Broy","year":"1993","unstructured":"M. Broy, C. Facchi, R. Grosu, R. Hettler, H. Hussmann, D. Nazareth, F. Regensburger, O. Slotosch, and K. St\u00f8len. The Requirement and Design Specification Language SPECTRUM. An Informal Introduction. Version 1.0. Part i. Technical Report TUM-I9311, Technische Universit\u00e4t M\u00fcnchen. Institut f\u00fcr Informatik, Fakult\u00e4t f\u00fcr Informatik, TUM, 80290 M\u00fcnchen, Germany, May 1993."},{"key":"8_CR7","volume-title":"Technical Report TUM-I9312","author":"M. Broy","year":"1993","unstructured":"M. Broy, C. Facchi, R. Grosu, R. Hettler, H. Hussmann, D. Nazareth, F. Regensburger, O. Slotosch, and K. St\u00f8len. The Requirement and Design Specification Language SPECTRUM. An Informal Introduction. Version 1.0. Part ii. Technical Report TUM-I9312, Technische Universit\u00e4t M\u00fcnchen. Institut f\u00fcr Informatik, Fakult\u00e4t f\u00fcr Informatik, TUM, 80290 M\u00fcnchen, Germany, May 1993."},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"R. M. Burstall, J. A. Goguen The semantics of CLEAR, a specification language. In D. Bj\u00f8rner, editor, Proc. Advanced Course on Abstract Software Specification. LNCS, Springer, 1980.","DOI":"10.1007\/3-540-10007-5_41"},{"key":"8_CR9","unstructured":"J. Bohn, H. Hungar, Traverdi \u2014 Transformation and Verfication of Distributed Systems. This volume."},{"key":"8_CR10","unstructured":"D. Bj\u00f8rner, H. Langmaack, C.A.R. Hoare, Eds., Provably Correct Systems (Tech. Report, DTH Lyngby, 1993)."},{"key":"8_CR11","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1016\/0022-0000(87)90026-2","volume":"34","author":"M. Broy","year":"1987","unstructured":"M. Broy, Specification and top-down design of distributed systems, J. Comput. System Sci. 34 (1987) 236\u2013265.","journal-title":"J. Comput. System Sci."},{"key":"8_CR12","first-page":"33","volume":"335","author":"M. Broy","year":"1988","unstructured":"M. Broy. Requirement and Design Specification for Distributed Systems. LNCS, 335:33\u201362, 1988.","journal-title":"LNCS"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"M. Broy. Methodische Grundlagen der Programmierung. In M. Broy, editor, Informatik und Mathematik, pages 355\u2013365. Springer-Verlag, 1991.","DOI":"10.1007\/978-3-642-76677-0_26"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"J.W. de Bakker, W.-P. de Roever, G. Rozenberg, Eds., Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, LNCS 430 (Springer-Verlag, 1990).","DOI":"10.1007\/3-540-52559-9"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press, 1990.","DOI":"10.1017\/CBO9780511624193"},{"key":"8_CR16","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986."},{"key":"8_CR17","unstructured":"J. Camilleri. The HOL System Description, Version 1 for HOL 88.1.10. Technical Report, Cambridge Research Center, 1989."},{"key":"8_CR18","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, A.P. Sistla, Automatic Verification of finite-state concurrent systems using temporal logic specifications, ACM TOPLAS 8 (1986) 244\u2013263.","journal-title":"ACM TOPLAS"},{"key":"8_CR19","unstructured":"I. Cla\u00dfen, H. Ehrig, and D. Wolz. Algebraic Specification Techniques and Tools for Software Development \u2014 The ACT Approach. World Scientific Publishing, AMAST Series in Computing, 1993, to appear."},{"key":"8_CR20","unstructured":"S. Conrad, M. Gogolla, and R. Herzig. Troll light: A Core Language for Specifying Objects. Informatik-Bericht 92-02, Technische Universit\u00e4t Braunschweig, 1992."},{"issue":"1","key":"8_CR21","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/320434.320440","volume":"1","author":"P. Chen","year":"1976","unstructured":"P. Chen. The Entity-Relationship Model \u2014 Towards a Unified View of Data. ACM Trans. on Database Systems, 1(1):9\u201336, 1976.","journal-title":"ACM Trans. on Database Systems"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Felix Cornelius, Heinrich Hu\u00dfmann, and Michael L\u00f6we. The korso Case Study for Software Engineering with Formal Methods, 1994. This volume.","DOI":"10.1007\/BFb0015474"},{"key":"8_CR23","unstructured":"Ingo Cla\u00dfen. Semantik der revidierten Version der algebraischen Spezifikationssprache ACT ONE. Technical Report 88\/24, TU Berlin, 1988."},{"key":"8_CR24","unstructured":"I. Cla\u00dfen. ACT System \u2014 User Manual. Internal Report, TU Berlin, April 1992."},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"K.M. Chandy, J. Misra, Parallel Program Design: A Foundation, Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"8_CR26","unstructured":"S. Conrad. Spezifikation eines vereinfachten Datenbanksystems. In Ehrich [Ehr93]."},{"issue":"4","key":"8_CR27","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1145\/6041.6042","volume":"17","author":"L. Cardelli","year":"1985","unstructured":"L. Cardelli and P. Wegner. On Understanding Types, Data Abstraction, and Polymorphism. ACM Computing Surveys, 17(4):471\u2013523, December 1985.","journal-title":"ACM Computing Surveys"},{"key":"8_CR28","unstructured":"E. Downs, P. Clare, and I. Coe. Structured systems analysis and design method (2nd ed). Prentice-Hall, 1992."},{"key":"8_CR29","unstructured":"K. Didrich, A. Fett, C. Gerke, W. Grieskamp. P. Pepper. Opal: Design and Implementation of an Algebraic Programming Language. accepted for Conference on Programming Languages and System Architecture"},{"key":"8_CR30","unstructured":"W. Damm, R. Schl\u00f6r, Specification and verification of system-level hardware designs using timing diagrams, in: Proc. European Design Automation Conference, Paris, 1993."},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"H.-D. Ehrich, G. Denker, and A. Sernadas. Constructing Systems as Object Communities. In M.-C. Gaudel and J.-P. Jouannaud, editors, Proc. TAPSOFT'93: Theory and Practice of Software Development, pages 453\u2013467. Springer LNCS 668, 1993.","DOI":"10.1007\/3-540-56610-4_82"},{"issue":"2","key":"8_CR32","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1016\/0169-023X(92)90008-Y","volume":"9","author":"G. Engels","year":"1992","unstructured":"G. Engels, M. Gogolla, U. Hohenstein, K. H\u00fclsmann, P. L\u00f6hr-Richter, G. Saake, and H.-D. Ehrich. Conceptual Modelling of Database Applications Using an Extended ER Model. Data & Knowledge Engineering, 9(2):157\u2013204, 1992.","journal-title":"Data & Knowledge Engineering"},{"key":"8_CR33","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-94709-3","volume-title":"Algebraische Spezifikation abstrakter Datentypen \u2014 Eine Einf\u00fchrung in die Theorie","author":"H.-D. Ehrich","year":"1989","unstructured":"H.-D. Ehrich, M. Gogolla, and U.W. Lipeck. Algebraische Spezifikation abstrakter Datentypen \u2014 Eine Einf\u00fchrung in die Theorie. Teubner, Stuttgart, 1989."},{"key":"8_CR34","unstructured":"H.-D. Ehrich, editor. Beitr\u00e4ge zu Korso-und Troll light-Fallstudien. Informatik-Bericht 93-11, Technische Universit\u00e4t Braunschweig, 1993."},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1. Springer, 1985.","DOI":"10.1007\/978-3-642-69962-7"},{"key":"8_CR36","first-page":"995","volume-title":"Handbook of Theoretical Computer Science, Vol. B","author":"E.A. Emerson","year":"1990","unstructured":"E.A. Emerson. Temporal and Modal Logic. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, pages 995\u20131072. North-Holland, Amsterdam, 1990."},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"H.-D. Ehrich and A. Sernadas. Fundamental Object Concepts and Constructions. In G. Saake and A. Sernadas, editors, Information Systems \u2014 Correctness and Reusability, Proc. ESPRIT BRA IS-CORE Workshop, London, pages 1\u201324. Informatik-Bericht 91-03, Technische Universit\u00e4t Braunschweig, 1991.","DOI":"10.1007\/978-3-642-77312-9_1"},{"key":"8_CR38","doi-asserted-by":"crossref","unstructured":"K. Futatsugi, J.A. Goguen, J.-P. Jouannaud, J. Meseguer. Principles of OBJ2. In Proc. POPL, 1985.","DOI":"10.1145\/318593.318610"},{"key":"8_CR39","unstructured":"J. Fiadeiro, C. Sernadas, T. Maibaum, and A. Sernadas. Describing and Structuring Objects for Conceptual Schema Development. In Loucopoulos and Zicari [LZ92], pages 117\u2013138."},{"key":"8_CR40","unstructured":"M.-C. Gaudel. Towards Structured Algebraic Specifications. ESPRIT \u201885', Status Report of Continuing Work (North-Holland), pages 493\u2013510, 1986."},{"key":"8_CR41","unstructured":"M. Gogolla, S. Conrad, G. Denker, R. Herzig, N. Vlachantonis, and H.-D. Ehrich. Troll light The Language and Its Development Environment. This volume."},{"key":"8_CR42","unstructured":"J. Goguen, D. Coleman, and R. Gallimore. Applications of Algebraic Specifications using OBJ. Cambridge, 1992."},{"key":"8_CR43","doi-asserted-by":"crossref","unstructured":"M. Gogolla, S. Conrad, and R. Herzig. Sketching Concepts and Computational Model of Troll light. In A. Miola, editor, Proc. 3rd Int. Conf. Design and Implementation of Symbolic Computation Systems DISCO, pages 17\u201332. Springer LNCS 722, 1993.","DOI":"10.1007\/BFb0013165"},{"key":"8_CR44","unstructured":"R. Grosu, R. Hettler, D. Nazareth, F. Regensburger, and O. Slotosch. The specification language Spectrum \u2014 Language Report V1.0. Technical Report TUM-I9429, Technische Universit\u00e4t M\u00fcnchen. Institut f\u00fcr Informatik, 1994."},{"key":"8_CR45","volume-title":"Technical report","author":"J.V. Guttag","year":"1985","unstructured":"J.V. Guttag, J.J. Horning, and J.M. Wing. Larch in Five Easy Pieces. Technical report, Digital, Systems Research Center, Paolo Alto, California, 1985."},{"key":"8_CR46","doi-asserted-by":"crossref","unstructured":"J.A. Goguen and J. Meseguer. Unifying Functional, Object-Oriented and Relational Programming with Logical Semantics. Research Directions in Object-Oriented Programming, B. Shriver, P. Wegner, (eds.), pages 417\u2013477. MIT Press, 1987.","DOI":"10.1145\/323779.323755"},{"key":"8_CR47","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"8_CR48","unstructured":"R. Grosu and D. Nazareth. Towards a New Way of Parameterization. In Proceedings of the Third Maghrebian Conference on Software Engineering and Artificial Intelligence, pages 383\u2013392, 1994."},{"key":"8_CR49","unstructured":"Radu Grosu and Franz Regensburger. The Logical Framework of Spectrum. Technical Report TUM-I9402, Institut f\u00fcr Informatik, Technische-Universit\u00e4t M\u00fcnchen, 1994."},{"key":"8_CR50","unstructured":"OPAL Language Group. The Programming Language OPAL. Technical Report 91-10, Technische Universit\u00e4t Berlin, 1991."},{"key":"8_CR51","volume-title":"Compositional Description of Object Communities with Troll light","author":"R. Herzig","year":"1994","unstructured":"R. Herzig, S. Conrad, and M. Gogolla. Compositional Description of Object Communities with Troll light. In C. Chrisment, editor, Proc. Basque Int. Workshop on Information Technology (BIWIT). Cepadues Society Press, France, 1994."},{"key":"8_CR52","unstructured":"M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988."},{"key":"8_CR53","unstructured":"R. Herzig, Spezifikation der abstrakten Syntax von TROLL light mit TROLL light. In Ehrich [Ehr93], pages 43\u201349."},{"key":"8_CR54","unstructured":"R. Hettler. A Requirement Specification for a Lexical Analyzer. Technical Report TUM-I9409, TU M\u00fcnchen, 1994."},{"key":"8_CR55","doi-asserted-by":"crossref","unstructured":"P. Hudak, S. Peyton Jones, and P. Wadler, editors. Report on the Programming Language Haskell, A Non-strict Purely Functional Language (Version 1.2). ACM SIGPLAN Notices, May 1992.","DOI":"10.1145\/130697.130699"},{"issue":"3","key":"8_CR56","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/45072.45073","volume":"19","author":"R. Hull","year":"1987","unstructured":"R. Hull and R. King. Semantic Database Modelling: Survey, Applications, and Research Issues. ACM Computing Surveys, 19(3):201\u2013260, 1987.","journal-title":"ACM Computing Surveys"},{"key":"8_CR57","unstructured":"R.W. Harper, D.B. MacQueen, and R.G. Milner. Standard ML. Report ECS-LFCS-86-2, Univ. Edinburgh, 1986."},{"key":"8_CR58","doi-asserted-by":"crossref","unstructured":"R. Hettler, D. Nazareth, F. Regensburger, and O. Slotosch. AVL trees revisited: A case study in Spectrum, 1994. This volume.","DOI":"10.1007\/BFb0015459"},{"key":"8_CR59","unstructured":"H. Hungar, G, R\u00fcnger, Verification of a communication network. A case study in the use of temporal logic, Manuscript, Oldenburg\/Saarbr\u00fccken, 1993."},{"key":"8_CR60","doi-asserted-by":"crossref","unstructured":"H. Hungar, Combining model checking and theorem proving to verify parallel processes, in: C. Courcoubetis, Ed., Computer Aided Verification (CAV '93), LNCS 697 (Springer-Verlag, 1993) 154\u2013165.","DOI":"10.1007\/3-540-56922-7_13"},{"key":"8_CR61","unstructured":"H. Hussmann. Rapid Propotyping for Algebraic Specifications \u2014 RAP-System User's Manual Tech. Report MIP-8504, Universit\u00e4t Passau 1985 (revised edition 1987."},{"key":"8_CR62","unstructured":"H. Hussmann. Synergy between formal and pragmatic software engineering methods. Technical Report TUM-I9323, Institut f\u00fcr Informatik, Technische-Universit\u00e4t M\u00fcnchen, September 1993. (Submitted to ESOP 94)."},{"key":"8_CR63","unstructured":"H. Hu\u00dfmann. Formal Foundation for SSADM. Habilitation thesis, TU M\u00fcnchen, 1994."},{"key":"8_CR64","series-title":"FZI Publication 1\/94","volume-title":"Case Study \u201cProduction Cell\u201d: A Comparative Study in Formal Specification and Verification","author":"R. Herzig","year":"1994","unstructured":"R. Herzig and N. Vlachantonis. Specification of a Production Cell with TROLL light, Case Study \u201cProduction Cell\u201d: A Comparative Study in Formal Specification and Verification (C. Lewerentz and T. Lindner, eds.), Chapter 14. FZI Publication 1\/94, Forschungszentrum Informatik, Karlsruhe (Germany), 1994."},{"key":"8_CR65","unstructured":"INMOS Ltd., Occam 2 Reference Manual (Prentice Hall, 1988)."},{"key":"8_CR66","doi-asserted-by":"crossref","unstructured":"B. Josko, Modelchecking of Ctl formulae under liveness assumptions, in: Proc. ICALP 87, LNCS 267 (Springer-Verlag, 1987) 280\u2013289.","DOI":"10.1007\/3-540-18088-5_23"},{"key":"8_CR67","doi-asserted-by":"crossref","unstructured":"B. Josko, Verifying the correctness of AADL modules using model checking, in: [BRR89] 386\u2013400.","DOI":"10.1007\/3-540-52559-9_72"},{"key":"8_CR68","unstructured":"R. Jungclaus, G. Saake, T. Hartmann, and C. Sernadas. Object-Oriented Specification of Information Systems: The TROLL Language. Informatik-Bericht 91-04, Technische Universit\u00e4t Braunschweig, 1991."},{"key":"8_CR69","unstructured":"B. Krieg-Br\u00fcckner and B. Hoffmann, editors. PROgram development by SPECification and TRAnsformation: Vol. I: Methodology, Vol II: Language Family, Vol III: System. Prospectra Report M.1.1.S3-R-55.2,-56.2,h-57.2. (to appear in LNCS), 1991. Universit\u00e4t Bremen (1990)."},{"key":"8_CR70","doi-asserted-by":"crossref","unstructured":"S. Kleuker, Case study: stepwise development of a communication processor using trace logic, to appear in: D.J. Andrewa, J.F. Groote, C.A. Middelburg, Eds., Semantics of Specification Languages (SoSL), Workshops in Computing, Springer-Verlag, 1994.","DOI":"10.1007\/978-1-4471-3229-5_14"},{"key":"8_CR71","first-page":"131","volume-title":"LNCS 332","author":"T. Lehmann","year":"1987","unstructured":"T. Lehmann and J. Loeckx. The Specification Language of OBSCURE. Recent Trends in Data Type Specification, Selected Papers of the 5th Workshop on Specification of Abstract Data Types, pages 131\u2013153. LNCS 332, Springer-Verlag, Berlin 1987."},{"key":"8_CR72","unstructured":"C. Lewerentz and T. Lindner. Case Study\u2019 Production Cell': A Comparative Study in Formal Specification and Verification. This volume."},{"key":"8_CR73","unstructured":"P. Loucopoulos. Conceptual Modeling. In Loucopoulos and Zicari [LZ92], pages 1\u201326."},{"key":"8_CR74","unstructured":"Z. Luo, R. Pollack, and P. Taylor. How to Use LEGO. Departement of Computer Science, University of Edinburgh, 1989."},{"key":"8_CR75","unstructured":"N.A. Lynch and M.R. Tuttle, An introduction to input\/ouput automata, CWI-Quaterly 2(3), CWI, 1989."},{"key":"8_CR76","unstructured":"P. Loucopoulos and R. Zicari, editors. Conceptual Modeling, Databases, and CASE: An Integrated View of Information Systems Development. John Wiley & Sons, 1992."},{"key":"8_CR77","unstructured":"W. Menzel et al. Bestandsaufnahme und Klassifikation der Korso-Werkzeuge. Technischer Bericht, Universit\u00e4t Karlsruhe 1993."},{"key":"8_CR78","unstructured":"R. Milner, Communication and Concurrency (Prentice-Hall, 1989)."},{"key":"8_CR79","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Vol. 1: Specification. Springer, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"8_CR80","unstructured":"F. Nickl. Ablaufspezifikation durch Datenflu\u00dfmodellierung und stromverarbeitende Funktionen. Technical Report TUM-I9334, Technische Universit\u00e4t M\u00fcnchen, 1993."},{"key":"8_CR81","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/BF01887212","volume":"1","author":"T. Nipkow","year":"1989","unstructured":"T. Nipkow. Term Rewriting and Beyond \u2014 Theorem Proving in Isabelle. FAC, 1:320\u2013338, 1989.","journal-title":"FAC"},{"key":"8_CR82","unstructured":"T. Nipkow. Order-Sorted Polymorphism in Isabelle. In G. Huet, G. Plotkin, and C. Jones, editors, Proc. 2nd Workshop on Logical Frameworks, pages 307\u2013321, 1991."},{"key":"8_CR83","doi-asserted-by":"crossref","unstructured":"T. Nipkow and C. Prehofer. Type Checking Type Classes. In Proc. 20th ACM Symp. Principles of Programming Languages, pages 409\u2013418. ACM Press, 1993.","DOI":"10.1145\/158511.158698"},{"key":"8_CR84","doi-asserted-by":"crossref","unstructured":"E.-R. Olderog, Nets, Terms and Formulas (Cambridge University Press, 1991).","DOI":"10.1017\/CBO9780511526589"},{"key":"8_CR85","doi-asserted-by":"crossref","unstructured":"E.-R. Olderog and S. R\u00f6ssig, A case study in transformational design of concurrent systems, in: M.-C. Gaudel, J.-P. Jouannaud, Eds., Proc. TAP-SOFT '93, LNCS 668 (Springer-Verlag, 1993) 90\u2013104.","DOI":"10.1007\/3-540-56610-4_58"},{"key":"8_CR86","unstructured":"E.-R. Olderog and S. R\u00f6ssig and J. Sander and M. Schenke, ProCoS at Oldenburg: The Interface between Specification Language and Occam-like Programming Language, Bericht 3\/92, Univ. Oldenburg, Fachbereich Informatik, 1992."},{"key":"8_CR87","doi-asserted-by":"crossref","unstructured":"L.C. Paulson. Logic and Computation, Interactive Proof with Cambridge LCF, volume 2 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"8_CR88","unstructured":"N. Perry. Hope+. Internal report IC\/FPRC\/LANG\/2.51\/7, Dept. of Computing, Imperial College London, 1988."},{"issue":"3","key":"8_CR89","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1145\/62061.62062","volume":"20","author":"J. Peckham","year":"1988","unstructured":"J. Peckham and F. Maryanski. Semantic Data Models. ACM Computing Surveys, 20(3):153\u2013189, 1988.","journal-title":"ACM Computing Surveys"},{"key":"8_CR90","unstructured":"C. Pusch. \u00dcbersetzung von Spectrum Spezifikationen nach Isabelle. Fortgeschrittenenpraktikum, Technische Universit\u00e4t M\u00fcnchen, 1994."},{"key":"8_CR91","unstructured":"Franz Regensburger. The calculus of Spectrum. Technical Report TUM-I9424, Institut f\u00fcr Informatik, Technische-Universit\u00e4t M\u00fcnchen, 1994."},{"key":"8_CR92","doi-asserted-by":"crossref","unstructured":"W. Reisig. Petri Nets: An Introduction. Springer, 1985.","DOI":"10.1007\/978-3-642-69968-9"},{"key":"8_CR93","unstructured":"L. Rapanotti and A. Socorro. Introducing FOOPS. Technical Report, Programming Research Group, Oxford University, 1992."},{"key":"8_CR94","unstructured":"M. Schulte, Spezifikation und Verifikation von kommunizierenden Objekten in einem verteilten System, Diplomarbeit, Fachbereich Informatik, Univ. Oldenburg, M\u00e4rz 1994."},{"key":"8_CR95","unstructured":"R. Schl\u00f6r, J. Helbig, Layered timing diagrams \u2014 visual constraint programming for system level design, submitted to publication, 1993."},{"key":"8_CR96","unstructured":"C. Sudergat, R. Hettler, D. Nazareth, and F. Regensburger. AVL-Trees: A case study for software development in spectrum. Interner Bericht der TU M\u00fcnchen, 1993."},{"key":"8_CR97","unstructured":"J.M. Spivey, The Z Notation: A Reference Manual (Prentice Hall, 1989)."},{"key":"8_CR98","unstructured":"A. Sernadas, C. Sernadas, and H.-D. Ehrich. Object-Oriented Specification of Databases: An Algebraic Approach. In P.M. Stocker and W. Kent, editors, Proc. 13th Int. Conf. on Very Large Data Bases VLDB, pages 107\u2013116. Morgan-Kaufmann, 1987."},{"key":"8_CR99","volume-title":"Tech. Report","author":"A. Sernadas","year":"1991","unstructured":"A. Sernadas, C. Sernadas, P. Gouveia, P. Resende, and J. Gouveia. OBLOG \u2014 Object-Oriented Logic: An Informal Introduction. Tech. Report, INESC, Lisbon, 1991."},{"key":"8_CR100","doi-asserted-by":"crossref","unstructured":"D. Sannella, A. Tarlecki On Observational Equivalence. Journal of Comp. and Sys. Science, 34, 1987.","DOI":"10.1016\/0022-0000(87)90023-7"},{"key":"8_CR101","unstructured":"C. Strachey. Fundamental Concepts in Programming Languages. In Lecture Notes for International Summer School in Computer Programming, Copenhagen, 1967."},{"key":"8_CR102","volume-title":"Technical Report CSR-131-83","author":"D.T. Sannella","year":"1983","unstructured":"D.T. Sannella and M. Wirsing. A Kernel Language for Algebraic Specification and Implementation. Technical Report CSR-131-83, University of Edinburgh, Edinburgh EH9 3JZ, September 1983."},{"key":"8_CR103","doi-asserted-by":"crossref","unstructured":"D. A. Turner. Miranda \u2014 a Non-Strict Functional Language with Polymorphic Types. In Jouannaud, editor, Conference on Functional Programming Languages and Computer Architecture, pages 1\u201316. Springer Verlag, 1985.","DOI":"10.1007\/3-540-15975-4_26"},{"key":"8_CR104","series-title":"LNCS 685","first-page":"463","volume-title":"Advanced Information Systems Engineering, Proc. 5th CAiSE'93","author":"N. Vlachantonis","year":"1993","unstructured":"N. Vlachantonis, R. Herzig, M. Gogolla, G. Denker, S. Conrad, and H.-D. Ehrich. Towards Reliable Information Systems: The Korso Approach. In C. Rolland, F. Bodart, and C. Cauvet, editors, Advanced Information Systems Engineering, Proc. 5th CAiSE'93, Paris, pages 463\u2013482. Springer LNCS 685, 1993."},{"key":"8_CR105","doi-asserted-by":"crossref","unstructured":"P. Wadler and S. Blott. How to Make Ad-hoc Polymorphism Less Ad hoc. In 16th ACM Symposium on Principles of Programming Languages, pages 60\u201376, 1989.","DOI":"10.1145\/75277.75283"},{"key":"8_CR106","doi-asserted-by":"crossref","unstructured":"Uwe Wolter, K. Didrich, Felix Cornelius, M. Klar, R. Wess\u00e4ly, and H. Ehrig. How to Cope with the Spectrum of Spectrum, 1994. This volume.","DOI":"10.1007\/BFb0015461"},{"key":"8_CR107","unstructured":"C. Wadsworth, M. Gordon, and R. Milner. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of LNCS. Springer, 1979."},{"key":"8_CR108","unstructured":"R.J. Wieringa. A Conceptual Model Specification Language (CMSL, Version 2). Technical Report IR-267, Vrije Universiteit Amsterdam, 1991."},{"key":"8_CR109","unstructured":"N. Wirth. Algorithms + Data Structures = Programs. Prentice Hall, 1976."},{"key":"8_CR110","first-page":"677","volume-title":"Handbook of Theoretical Computer Science, Vol. B","author":"M. Wirsing","year":"1990","unstructured":"M. Wirsing. Algebraic Specification. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, Vol. B, pages 677\u2013788. North-Holland, Amsterdam, 1990."},{"key":"8_CR111","unstructured":"M. Wirsing et al. A Framework for Software Development in Korso. Informatik-Bericht, LMU M\u00fcnchen, 1992."},{"key":"8_CR112","unstructured":"J. Zwiers, Compositionality, Concurrency, and Partial Correctness \u2014 Proof Theories for Networks of Processes and Their Relationship, LNCS 321 (Springer-Verlag, 1989)."}],"container-title":["Lecture Notes in Computer Science","KORSO: Methods, Languages, and Tools for the Construction of Correct Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0015460","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T10:58:39Z","timestamp":1683284319000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0015460"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540605898","9783540478027"],"references-count":112,"URL":"https:\/\/doi.org\/10.1007\/bfb0015460","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}