This monograph details several important advances in the area known as the proofs-as-programs paradigm, a set of approaches to developing programs from proofs in constructive logic. It serves the dual purpose of providing a state-of-the-art overview of the field and detailing tools and techniques to stimulate further research.

One of the booka (TM)s central themes is a general, abstract framework for developing new systems of program synthesis by adapting proofs-as-programs to new contexts, which the authors call the Curry--Howard Protocol. This protocol is used to provide two novel applications for industrial-scale, complex software engineering: contractual imperative program synthesis and structured software synthesis. These applications constitute an exemplary justification for the applicability of the protocol to different contexts.

The book is intended for graduate students in computer science or mathematics who wish to extend their background in logic and type theory as well as gain experience working with logical frameworks and practical proof systems. In addition, the proofs-as-programs research community, and the wider computational logic, formal methods and software engineering communities will benefit. The applications given in the book should be of interest for researchers working in the target problem domains.

Service-Oriented Computing is a paradigm for developing and providing software that can address many IT challenges, ranging from integrating legacy systems to building new, massively distributed, interoperable, evaluable systems and applications. The widespread use of SOC demonstrates the practical benefits of this approach. Furthermore it raises the standard for reliability, security, and performance for IT providers, system integrators, and software developers. This book documents the main results of Sensoria, an Integrated Project funded by the European Commission in the period 2005-2010. The book presents, as Sensoria's essence, a novel, coherent, and comprehensive approach to the design, formal analysis, automated deployment, and reengineering of service-oriented applications. Following a motivating introduction, the 32 chapters are organized in the following topical parts: modeling in service-oriented architectures; calculi for service-oriented computing; negotiation, planning, and reconfiguration; qualitative analysis techniques for SOC; quantitative analysis techniques for SOC; model-driven development and reverse engineering for service-oriented systems; and case studies and patterns.

This monograph details several important advances in the direction of a practical proofs-as-programs paradigm, which constitutes a set of approaches to developing programs from proofs in constructive logic with applications to industrial-scale, complex software engineering problems. One of the books central themes is a general, abstract framework for developing new systems of programs synthesis by adapting proofs-as-programs to new contexts.

This book constitutes the refereed proceedings of the 12th International Conference on Fundamental Approaches to Software Engineering, FASE 2009, held in York, UK, in March 2009, as part of ETAPS 2009, the European Joint Conferences on Theory and Practice of Software.

The 30 revised full papers presented together with 2 tool demonstrations were carefully reviewed and selected from 123 regluar and 9 tool paper submissions. The topics addressed are model-driven development, synthesis and adaptation, modeling, testing and debugging, model analysis, patterns, security, queries and error handling, and tools (demos) and program analysis.

Software-intensive systems have become increasingly important for a multitude of products and services from all sectors of the economy, our national and - ternational infrastructure, and our daily lives. The ongoing decrease in size and cost of microprocessorsandstoragedevicesis leading to the development of ever more distributed and decentralized systems. Systems are assembled as dynamic federationsofautonomousandevolvingcomponents insteadof monolithicapp- cations, they perform tasks of staggering complexity with continuously cha- ing requirements and in a permanently evolving environment. In the near - ture novel technologies will allow the construction of systems with millions of nodes, and systems will be likely to containsubsystems basedonnew computing paradigms such as molecular computing. To identify these emergent trends, their impact on the information society in the next 10-15 years, and the challenges they present to computing, software engineering, cognition and intelligence, the European Commission has estab- 1 lished two Coordinated Actions: initially the project "Beyond the Horizon" 2 and then, starting in 2006, the project "InterLink" . Both projects are coor- nated by the European Research Consortium for Informatics and Mathematics (ERCIM EEIG) and funded by the Future and Emerging Technologies (FET) Unit of the European Commission. The ongoing project InterLink is composed of three thematic working groups: software-intensive systems and new comp- ingparadigms;ambientcomputingandcommunicationenvironments;intelligent and cognitive systems. This volume presents the results of the working group on software-intensive systemsandnovelcomputing paradigms.Theobjectivewasto imaginethela- scape in which the next generations of software-intensive systems will operate.

This volume contains the proceedings of ICTAC 2005, the second ICTAC, International Colloquium on Theoretical Aspects of Computing. ICTAC 2005 took place in Hanoi, Vietnam, October 17-21, 2005. ICTAC was founded by the International Institute for Software Technology of the United Nations University (UNU-IIST) to serve as a forum for practiti- ers, lecturers and researchers from academia, industry and government who are interested in theoretical aspects of computing and rigorous approaches to so- ware engineering. The colloquium is aimed particularly, but not exclusively, at participants from developing countries. We believe that this will help developing countries to strengthen their research, teaching and development in computer science and engineering, improve the links between developing countries and developed countries, and establish collaboration in research and education. By providingavenueforthediscussionofcommonproblemsandtheirsolutions, and for the exchangeof experiencesand ideas, this colloquiumsupportsresearchand development in computer science and software technology. ICTAC is attracting more and more attention from more and more countrie

Web engineering is a new discipline that addresses the pressing need for syst- atic and tool-supported approaches for the development, maintenance and te- ing of Web applications. Web engineering builds upon well-known and succe- ful software engineering principles and practices, adapting them to the special characteristics of Web applications. Even more relevant is the enrichment with methods and techniques stemming from related areas like hypertext authoring, human-computer interaction, content management, and usability engineering. The goal of the 4th International Conference on Web Engineering (ICWE 2004), inlinewiththepreviousICWEconferences, wastoworktowardsabetterund- standing of the issues related to Web application development. Special attention was paid to emerging trends, technologies and future visions, to help the a- demic and industrial communities identify the most challenging tasks for their research and projects. Following a number of successful workshops on Web engineering since 1997 at well-known conferences, such as ICSE and WWW, the ?rst conference on Web engineering was held in C aceres, Spain in 2001. It was followed by ICWE 2002 in Santa Fe, Argentina and ICWE 2003 in Oviedo, Spain. In 2004 ICWE moved to the center of Europe and was held in Munich, Germany from July 26 to 30. ICWE 2004 was organized by the Institute for Informatics of the Ludwig- Maximilians-Universit] at (LMU) Munich. The ICWE 2004 edition received a total of 204 submissions, out of which 25 paperswereselectedbytheProgramCommitteeasfullpapers(12%acceptance)."

This volume contains the papers from the workshop "Radical Innovations of Software and Systems Engineering in the Future." This workshop was the ninth in the series of Monterey Software Engineering workshops for formulating and advancing software engineering models and techniques, with the fundamental theme of increasing the practical impact of formal methods. During the last decade object orientation was the driving factor for new system solutions in many areas ranging from e-commerce to embedded systems. New modeling languages such as UML and new programming languages such as Java and CASE tools have considerably in?uenced the system development techniques of today and will remain key techniques for the near future. However, actual practice shows many de?ciencies of these new approaches: - there is no proof and no evidence that software productivity has increased with the new methods; - UML has no clean scienti?c foundations, which inhibits the construction of powerful analysis and development tools; - support for mobile distributed system development is missing; - formanyapplications,object-orienteddesignisnotsuitedtoproducingclean well-structured code, as many applications show.

This volume contains selected papers from WADT 2002, the 16th International Workshop on Algebraic Development Techniques. Like its predecessors, WADT 2002 focussed on the algebraic approach to the speci?cation and development of systems, an area that was born around the algebraic speci?cation of abstract data types and encompasses today the formal design of software systems, new speci?cation frameworks and a wide range of application areas. WADT 2002 took place at the convent of Frauenchiemsee, Germany, on September 24 27, 2002, and was organized by Rolf Hennicker, Dirk Pattinson and Martin Wirsing. The workshop also included a special track on Formalism, Logic, Institution Relating, Translating and Structuring (FLIRTS), and three satelliteevents: ameetingoftheIFIP WorkingGroup1.3onFoundationsofS- tem Speci?cation, a Workshop on Global Computing organized by the AGILE project, and a Workshop on Multimedia Instruction in Safe and Secure Systems (MMISS). The program consisted of invited talks by Egidio Astesiano (Genoa, Italy), Andrew Gordon (Cambridge, UK), and Jan Rutten (Amsterdam, The Neth- lands), and 44 presentations describing ongoing research on main topics of the workshop: formal methods for system development, speci?cation languages and methods, systems and techniques for reasoning about speci?cations, speci?- tion development systems, methods and techniques for concurrent, distributed and mobile systems, and algebraic and co-algebraic foundations."

This book constitutes the refereed proceedings of the 5th International Conference on Algebraic Methodology and Software Technology, AMAST '96, held in Munich, Germany, in July 1996.
The book presents 25 revised full papers selected from a total of 67 submissions and 23 system demonstrations; also included are six invited talks and six invited presentations of the AMAST Education Day on industrial applications of formal methods. The full papers are organized in topical sections on theorem proving, algebraic specification, concurrent and reactive systems, program verification, logic programming and term rewriting, and algebraic and logical foundations.

This volume contains the papers accepted for presentation at the Fourth International Symposium on Programming Language Implementation and Logic Programming (PLILP '92) held in Leuven, Belgium, August 26-28, 1992. Theaim of the symposium was to explore new declarative concepts, methods and techniques relevant for implementation of all kinds of programming languages, whether algorithmic or declarative. The symposium gathered researchers from the fields of algorithmic programming languages as well as logic, functional, and object-oriented programming. The topics discussed in the volume include: - Declarative implementation techniques; - Implementation of declarative concepts and modules; - Compiler specification and construction; - Program transformation; - Programming environments for declarative languages; - Amalgamation of logic programming with algorithmic, functional, or object-oriented techniques; - Executable specification.

The systematic development of software systems is a central task of computing science. A software system is the result of putting together knowledge about the application, the requirements and the structures of computing science. Under the heading CIP (Computer-aided Intuition-guided Programming), a group of researchers led by Prof. F.L. Bauer and Prof. K. Samelson started work in 1975 in the direction of formal program specification, transformational programming, and tool supportfor program development. The collection of papers in this volume presents examples of a formal approach to programming language concepts and program development based on algebraic specifications and program transformations. Examples are also presented of evolutions and modificationsof the original ideas of the CIP project. The topics range from descriptionsof the program development process to derivations of algorithms from specifications. The volume is dedicated to Prof. F.L. Bauer.

This volume contains the papers which have been accepted for presentation atthe Third International Symposium on Programming Language Implementation andLogic Programming (PLILP '91) held in Passau, Germany, August 26-28, 1991. The aim of the symposium was to explore new declarative concepts, methods and techniques relevant for the implementation of all kinds of programming languages, whether algorithmic or declarative ones. The intention was to gather researchers from the fields of algorithmic programming languages as well as logic, functional and object-oriented programming. This volume contains the two invited talks given at the symposium by H. Ait-Kaci and D.B. MacQueen, 32 selected papers, and abstracts of several system demonstrations. The proceedings of PLILP '88 and PLILP '90 are available as Lecture Notes in Computer Science Volumes 348 and 456.

This volume contains the presentations of the Fifth Symposium on Theoretical Aspects of Computer Science (STACS 88) held at the University of Bordeaux, February 11-13, 1988. In addition to papers presented in the regular program the volume contains abstracts of software systems demonstrations which were included in this conference series in order to show applications of research results in theoretical computer science. The papers are grouped into the following thematic sections: algorithms, complexity, formal languages, rewriting systems and abstract data types, graph grammars, distributed algorithms, geometrical algorithms, trace languages, semantics of parallelism.

This book constitutes the proceedings of the 6th European Conference on Massive Open Online Courses, EMOOCs 2019, held in Naples, Italy, in May 2019. The 15 full and 6 short papers presented in this volume were carefully reviewed and selected from 42 submissions. Massive Open Online Courses (MOOCs) have marked a milestone in the use of technology for education. The reach, potential, and possibilities of EMOOCs are immense. But they are not only restricted to global outreach: the same technology can be used to improve teaching on campus and training inside companies and institutions. The chapter 'Goal Setting and Striving in MOOCs. A Peek inside the Black Box of Learner Behaviour' is open access under a CC BY 4.0 license at link.springer.com.

This book constitutes the refereed proceedings of the 8th International Conference on Knowledge Science, Engineering and Management, KSEM 2015, held in Chongqing, China, in October 2015. The 57 revised full papers presented together with 22 short papers and 5 keynotes were carefully selected and reviewed from 247 submissions. The papers are organized in topical sections on formal reasoning and ontologies; knowledge management and concept analysis; knowledge discovery and recognition methods; text mining and analysis; recommendation algorithms and systems; machine learning algorithms; detection methods and analysis; classification and clustering; mobile data analytics and knowledge management; bioinformatics and computational biology; and evidence theory and its application.

A collective autonomic system consists of collaborating autonomic entities which are able to adapt at runtime, adjusting to the state of the environment and incorporating new knowledge into their behavior. These highly dynamic systems are also known as ensembles. To ensure correct behavior of ensembles it is necessary to support their development through appropriate methods and tools which can guarantee that an autonomic system lives up to its intended purpose; this includes respecting important constraints of the environment. This State-of-the-Art Survey addresses the engineering of such systems by presenting the methods, tools and theories developed within the ASCENS project. ASCENS was an integrated project funded in the period 2010-2015 by the 7th Framework Programme (FP7) of the European Commission as part of the Future Emerging Technologies Proactive Initiative (FET Proactive). The 17 contributions included in this book are organized in four parts corresponding to the research areas of the project and their concrete applications: (I) language and verification for self-awareness and self-expression, (II) modeling and theory of self-aware and adaptive systems, (III) engineering techniques for collective autonomic systems, and last but not least, (IV) challenges and feedback provided by the case studies of the project in the areas of swarm robotics, cloud computing and e-mobility.

Das Buch bietet eine knappe, praxisorientierte Einfuhrung in die Programmierung mit Java. Basierend auf Vorlesungen, Kursen und Praktika fur die ersten beiden Semester an der Ludwig-Maximilians-Universitat Munchen, sollen Leser moglichst schnell in die Lage versetzt werden, Java Programme zu verstehen und selbstandig zu schreiben. Das Buch umfasst den Stoff einer Erstsemester-Vorlesung oder eine Java-Umschulung und vermittelt damit die Grundlagen fur eine akademische Ausbildung oder fur einen beruflichen Einstieg als Java-Programmierer.

Dieses Buch uber elementare Aussagenlogik (wie auch seine geplante Fortsetzung uber Elementare Pradikatenlogik und Universelle Algebra) ist aus Vorlesungen an der Technischen Universitat Munchen entstanden. Es basiert auf der Uberzeugung, dass fur Studierende der Informatik nicht nur ein anderer Aufbau des mathematischen Grundstudiums geboten ist als etwa fur Ingenieure oder Physiker, sondern auch ein anderes Menu, als es sich an unseren Universitaten nach den GAMM-NTG-Empfehlungen der siebziger Jahre eingeburgert hat. Neben den unentbehrlichen Einfuhrungsvorlesungen in Mathematik sind fur die Informatiker vor dem Vordiplom handwerkliche Grundkenntnisse in Logik und Universeller Algebra erforderlich - als Grundlage fur die Praktische und die Theoretische Informatik im zweiten Studienabschnitt. Im Gegensatz zu vielen anderen Buchern uber Logik ist dieses fur den Anfanger der Informatik geschrieben und didaktisch auf sein Niveau eingestellt. Dabei sind sonst eher ausserhalb der Aussagenlogik liegende Gegenstande wie die Schaltlogik systematisch einbezogen worden, wo immer es moglich war: von dem fur die Programmiersprachen so wichtigen Gebiet der dyadischen Fallunterscheidungen uber die Resolventenmethode, die den Anschluss an die Pradikatenlogik vorbereitet, bis zu modalen Aussagenlogiken. Die eingestreuten Ubungsaufgaben greifen haufig Gedanken auf, die im Text nur nebenbei erwahnt sind, und stellen Querbezuge her. Die Losungshinweise am Ende des Buches bieten manche Uberraschungen.