## 2018 2017 2016 2015 2014 2013 2012 2011 2010 2009 2008 2007 2006 2005 2004 2003 2002 2001 2000 1999 1998 1997 1996 1995 1994 1993 1992 1991 1990 1989 1988 1987 1986 1985 1984 1983 1982 1981 1980 1979 1978 1977 1976 1975 1974 1973 1972 1971 1970 1969 1968 1967 1966 1965 1964 1963 1962 1960 1959 1958 1957 1956 1955 1953 1952 1951 1950 1949 1948 1947 1946 1945 1941 1938 1923 1911

### Journal

David Galindo, Paz Morillo, and Carla Rífols. Improved certificate-based encryption in the standard model. In: Journal of Systems and Software, Nr: 7, Vol: 81, Pages: 1218-1226, Elsevier, 2008.

[ External URL ] [ Bibtex ]

M.A.J. van Gerven, P.J.F. Lucas, and Th.P. van der Weide. A Generic Qualitative Characterization of Independence of Causal Influence. In: International Journal of Approximate Reasoning, 2008, In press.

[ Missing PDF ] [ Bibtex ]

S.J. Overbeek, P. van Bommel, and H.A. (Erik) Proper. Matching Cognitive Characteristics of Actors and Tasks in Information Systems Engineering. In: Knowledge-Based Systems, 2008.

In daily practice, discrepancies may exist in the suitability match of actors and the tasks that have been allocated to them. A formal framework for cognitive matchmaking and a prototype implementation are introduced as a possible solution to improve the fit between actors and tasks. A case study has been conducted to clarify how the proposed cognitive matchmaking approach can be utilized in information systems engineering. The inductive-hypothetical research strategy has been applied as an overall research approach. A separate iteration of the strategy has been applied within the case study.

[ PDF ] [ Bibtex ]

Wolter Pieters, and Robert van Haren. Temptations of turnout and modernisation: e-voting discourses in the UK and the Netherlands. In: Journal of Information, Communication and Ethics in Society, Nr: 4, Vol: 5, Pages: 276-292, 2008.

[ Missing PDF ] [ Bibtex ]

### Book

P. van Bommel, S.J.B.A. (Stijn) Hoppenbrouwers, H.A. (Erik) Proper, and J. (Jeroen) Roelofs. Concepts and Strategies for Quality of Modeling. IGI Global Publishing, 2008.

A process-oriented framework (QoMo) is presented that aims to further the study of analysis and support of processes for modelling. The framework is strongly goal-oriented, and expressed largely by means of formal rules. The concepts in the framework are partly derived from the SEQUAL framework for quality of modelling. A number of modelling goal categories is discussed in view of SE-QUAL/QoMo, as well as a formal approach to the descrip-tion of strategies to help achieve those goals. Finally, a prototype implementation of the framework is presented as an illustration and proof of concept.

[ PDF ] [ Bibtex ]

Innovations in information Systems Modeling: Methods and Best practices. Advances in Database Research, IGI Global Publishing, 2008.

[ Missing PDF ] [ Bibtex ]

The Handbook of Research on Virtual Workplaces and the New Nature of Business Practices. Edited by: P. Zemliansky, and K. St-Amant. February, IGI Global Publishing, 2008.

[ Missing PDF ] [ Bibtex ]

### Chapter

Concepts and Strategies for Quality of Modeling. 2008.

A process-oriented framework (QoMo) is presented that aims to further the study of analysis and support of processes for modelling. The framework is strongly goaloriented, and expressed largely by means of formal rules. The concepts in the framework are partly derived from the SEQUAL framework for quality of modelling. A number of modelling goal categories is discussed in view of SEQUAL/ QoMo, as well as a formal approach to the description of strategies to help achieve those goals. Finally, a prototype implementation of the framework is presented as an illustration and proof of concept.

[ Missing PDF ] [ Bibtex ]

S.J. Overbeek, P. van Bommel, H.A. (Erik) Proper, and D.B.B. Rijsenbrij. Foundations and Applications of Intelligent Knowledge Exchange. In: The Handbook of Research on Virtual Workplaces and the New Nature of Business Practices, Edited by: P. Zemliansky, and K. St-Amant. Chapter 5, Pages: 53-69, March, 2008, ISBN 9781599048932.

Exchange of knowledge is becoming increasingly important to modern organizations. In this chapter is explained what this elementary knowledge exchange consists of and how a virtual workplace can support knowledge exchange between workers. A scenario from the medical domain illustrates how physicians can improve their knowledge exchange by utilizing the virtual workplace models introduced. Better adaptation to the rapidly changing nature of providing health care is a desirable effect of improved knowledge exchange between physicians. Explicit models concerning possible physical, social and digital contexts of knowledge exchange are discussed, as well as models which depict how knowledge relatedness enable intelligent knowledge exchange. Researchers studying virtual workplace models for industry and academic purposes belong to the intended audience of this chapter. Administrators of public sector or other non-profit agencies who wish to incorporate virtual workplace models and methods into their daily operations can also benefit from the contents discussed.

[ PDF ] [ Bibtex ]

Innovations in Information Systems Modeling: Methods and Best Practices. IGI Global Publishing, 2008.

[ Missing PDF ] [ Bibtex ]

### Conference

Andr\ and P. R. DArgenio. Significant Diagnostic Counterexamples in Probabilistic Model Checking. In: Haifa Verification Conference: 4th International Conference (HVC 08), Lect. Notes Comp. Sci., Vol: 5394, Pages: 129-148, 2008.

[ Missing PDF ] [ Bibtex ]

Miguel E. Andr\'es. Conditional Probabilities over Probabilistic and Nondeterministic Systems. In: Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference (TACAS , Lect. Notes Comp. Sci., Vol: 4963, Pages: 157-172, 2008.

[ Missing PDF ] [ Bibtex ]

Marko van Eekelen, Stefan ten Hoedt, Rene Schreurs, and Yaroslav Usenko. Analysis of a Session-Layer Protocol in mCRL2. Verification of a Real-Life Industrial Implementation. In: Proc. 12th Int. Workshop on Formal Methods for Industrial Critical Systems (FMICS 2007), Edited by: P. Merino, and S. Leue. Lect. Notes Comp. Sci., Vol: 4916, Pages: 182-199, Springer, 2008.

[ Missing PDF ] [ Bibtex ]

AHA: Amortized Heap Space Usage Analysis. In: Trends in Functional Programming Volume 8: Selected Papers of the $8^{th}$ International Symposium on Trends in Functional Programming (TFP, Pages: 36-53, 2008.

[ Missing PDF ] [ Bibtex ]

S.J.B.A. (Stijn) Hoppenbrouwers. Community-based ICT Development as a Multi-Player Game. In: What is an Organization? Materiality, Agency and Discourse, May, 2008.

In this paper, we advocate both the metaphorical and practical use of a gaming approach to the analysis, design, and support of the creative, collaborative, yet also strongly constrained processes that lead to formal models for use in ICT system development and business analysis. Making formal (i.e. rationalistic, mathematics-oriented) modeling accessible to people with little or no modeling expertise (i.e. people from the Organizational Participant communities) is becoming an urgent, critical issue in Business-IT alignment. Formal Modeling involves languages aspects (informal-formal language), which is commonly known, but also strong analytic and procedural aspects, which is often ignored in modeling studies and practice. Recent research has led to insights concerning the goal-driven, conversational nature of collaborative modeling processes. Human factors and interaction deserve to be accepted as primary in the study, design, and support (tooling) concerning operational (real-life) formal modeling processes. Taking the gaming approach to operational modeling has a number of advantages, both practical and methodological, and seems a promising context for study and development of methods and (importantly) digital tools for improving and supporting collaborative formal modeling.

[ PDF ] [ Bibtex ]

S.J.B.A. (Stijn) Hoppenbrouwers, P. van Bommel, and Aki Jarvinen. Method Engineering as Game Design: an Emerging HCI Perspective on Methods and CASE Tools. In: Proceedings of EMMSAD, June, 2008.

In the last half decade, there has been increasing interest in the process of information systems modeling, mostly focusing on improvement of quality, eciency, and control. While generic guidelines and phasing have been explored to a considerable extent, we are still a long way removed from in-depth understanding, full support, and adequate tooling with respect to operational modeling processes. Building on existing work in modeling methods and method engineering, we propose to expand the scope of modeling process research by taking a Human-Computer Interaction approach, viewing (situational) methods and their tool support, in combination with participants in operational process enactment, as an operational interaction system. More in particular, we discuss the merits of using the Game Metaphor as a clarifying and goal-setting view on the design of such interaction systems. Thus we approach Method Engineering as Game Design.

[ PDF ] [ Bibtex ]

2nd Central-European Functional Programming School, CEFP 2007. Edited by: Zolt\'an Horv\'ath. Lect. Notes Comp. Sci. # " Tutorial Series", Vol: 5161, Springer, 2008.

[ Missing PDF ] [ Bibtex ]

Leonard Lensink, Sjaak Smetsers, and Marko van Eekelen. Machine Checked Formal Proof of a Scheduling Protocol for Smartcard Personalization. In: Proc. 12th Int. Workshop on Formal Methods for Industrial Critical Systems (FMICS 2007), Edited by: P. Merino, and S. Leue. Lect. Notes Comp. Sci., Vol: 4916, Pages: 115-132, Springer, 2008.

[ Missing PDF ] [ Bibtex ]

20th International Conference on Advanced Information Systems Engineering, CAiSE 2008, Montpellier, France, June 16-20, 2008, Proceedings. Edited by: Z. Bellahsene, and Z. Bellahsene. Lecture Notes in Computer Science, Vol: 5074, June, Springer, Berlin, Germany, EU, 2008.

[ Missing PDF ] [ Bibtex ]

Proc. 12th Int. Workshop on Formal Methods for Industrial Critical Systems (FMICS 2007). Edited by: P. Merino, and S. Leue. Lect. Notes Comp. Sci., Vol: 4916, Springer, 2008.

[ Missing PDF ] [ Bibtex ]

Proc. 12th Int. Workshop on Formal Methods for Industrial Critical Systems (FMICS 2007). Edited by: P. Merino, and S. Leue. Lect. Notes Comp. Sci., Vol: 4916, Springer, 2008.

[ Missing PDF ] [ Bibtex ]

Maarten de Mol, Marko van Eekelen, and Rinus Plasmeijer. Proving Properties of Lazy Functional Programs with SPARKLE. In: 2nd Central-European Functional Programming School, CEFP 2007, Edited by: Zolt\'an Horv\'ath. Lect. Notes Comp. Sci. # " Tutorial Series", Vol: 5161, Pages: 41-86, Springer, 2008.

[ Missing PDF ] [ Bibtex ]

Maarten de Mol, Marko van Eekelen, and Rinus Plasmeijer. A Single-Step Term-Graph Reduction System for Proof Assistants. In: Applications of Graph Transformations with Industrial Relevance, Third International Symposium, AGTIVE 2007. Proceedings of Selected and Invited Papers, Edited by: Sch\. Lect. Notes Comp. Sci., Vol: 5088, Pages: 184-200, October, Springer, 2008.

[ Missing PDF ] [ Bibtex ]

Trends in Functional Programming Volume 8: Selected Papers of the $8^{th}$ International Symposium on Trends in Functional Programming (TFP. Edited by: Marco Morazán. Intellect Publishers, UK, 2008.

[ Missing PDF ] [ Bibtex ]

M.W. (Matthijs) van Roosmalen and S.J.B.A. (Stijn) Hoppenbrouwers. Supporting Corporate Governance with Enterprise Architecture and Business Rule Management: A Synthesis of Stability and Agility. , 2008.

Business rule management (BRM) and enterprise architecture (EA) both offer support for corporate governance. They do this in different ways, with EA emphasizing a stable framework while BRM offers more agility to the enterprise through control of changing business rules. This paper explores the combination of BRM and EA in deployment to support governance, and argues for a synthesis between the two. Such a synthesis offers an organization the benefits of both stability and overview demanded by regulatory bodies, as well as agility in the face of rapidly changing compliance demands.

[ PDF ] [ Bibtex ]

J. Nabukenya, P. van Bommel, and H.A. (Erik) Proper. Repeatable Collaboration Processes for Mature Organizational Policy Making. In: Proceedings of the 14th Collaboration Researchers' International Workshop on Groupware (CRWIG08), LNCS, September, 2008.

Organizational policy making processes are complex processes in which many people are involved. Very often the results of these processes are not what the different stakeholders intended. Since policies play a major role in key decision making concerning the future of organizations, our research aims at improving the policies on the basis of collaboration. In order to achieve this goal, we apply the practice of collaboration engineering to the field of organizational policy making. We use the thinklet as a basic building block for facilitating intervention to create a repeatable pattern of collaboration among people working together towards achieving a goal. Our case studies show that policy making processes do need collaboration support indeed and that the resulting policies can be expected to improve.

[ PDF ] [ Bibtex ]

S.J. Overbeek, P. van Bommel, and H.A. (Erik) Proper. Information Systems Engineering supported by Cognitive Matchmaking. In: 20th International Conference on Advanced Information Systems Engineering, CAiSE 2008, Montpellier, France, June 16-20, 2008, Proceedings, Lecture Notes in Computer Science, Vol: 5074, Pages: 495-509, June, 2008.

In daily practice, discrepancies may exist in the suitability match of actors and the tasks that have been allocated to them. Formal theory and the prototype of a cognitive matchmaker system are introduced as a solution to improve the fit between actors and tasks. A case study has been conducted to clarify how the proposed cognitive matchmaker system can be utilized in information systems engineering. The inductive-hypothetical research strategy has been applied when performing the case study.

[ PDF ] [ Bibtex ]

Applications of Graph Transformations with Industrial Relevance, Third International Symposium, AGTIVE 2007. Proceedings of Selected and Invited Papers. Edited by: Sch\. Lect. Notes Comp. Sci., Vol: 5088, October, Springer, 2008.

[ Missing PDF ] [ Bibtex ]

What is an Organization? Materiality, Agency and Discourse. May, 2008.

[ Missing PDF ] [ Bibtex ]

Proceedings of the 14th Collaboration Researchersâ€™ International Workshop on Groupware (CRWIG08). 2008.

[ Missing PDF ] [ Bibtex ]

Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference (TACAS . Lect. Notes Comp. Sci., Vol: 4963, Springer, 2008.

[ Missing PDF ] [ Bibtex ]

Proceedings of Workshop on Regulations Modeling and Deployment, in conjunction with CAiSE 2008. 2008.

[ Missing PDF ] [ Bibtex ]

Proceedings of EMMSAD. June, 2008.

[ Missing PDF ] [ Bibtex ]

Workshop proceedings of the 19th International Conference on Advanced Infromarion Systems Engineering: EMMSAD. Vol: 1, June, Radboud University Nijmegen, 2008.

[ Missing PDF ] [ Bibtex ]

Haifa Verification Conference: 4th International Conference (HVC 08). Lect. Notes Comp. Sci., Vol: 5394, Springer, 2008.

[ Missing PDF ] [ Bibtex ]

### Reports

Peter Achten, Marko van Eekelen, Maarten de Mol, and Rinus Plasmeijer. A Common Arrow Based Semantics for GEC and iData Applications. Technical report: ICIS-R08023, December, Radboud University Nijmegen, 2008.

State-based interactive applications, whether they run on the desktop or as a web application, can be considered as collections of interconnected editors of structured values that allow users to manipulate data. This is the view that is advocated by the GEC and iData toolkits, which offer a high level of abstraction to programming desktop and web GUI applications respectively. Special features of these toolkits are that editors have shared, persistent state, and that they handle events individually. In this paper we cast these toolkits within the Arrow framework and present a single, uniÃ‚Â¯ed semantic model that defines shared state and event handling. We study the properties of this EditorArrow model, and of editors in particular. Furthermore, we present the definedness properties of the combinators. A reference implementation of the EditorArrow model is given with some small program examples. We discuss formal reasoning about the model using the proof assistant Sparkle.

[ PDF ] [ Bibtex ]

Peter Achten, Pieter Koopman, and Marco T. MorazÃ¡n. Draft Proceedings of The Ninth Symposium on Trends in Functional Programming (TFP). Technical report: ICIS-R08007, May, Radboud University Nijmegen, 2008.

Draft proceedings TFP 2008.

[ PDF ] [ Bibtex ]

Luc Rutten, and M.C.J.D. van Eekelen. Efficient and Formally Proven Reduction of Large Integers by Small Moduli. Technical report: ICIS-R08001, February, Radboud University Nijmegen, 2008.

On $w$-bit processors which are much faster at multiplying two $w$-bit integers than at dividing $2w$-bit integers by $w$-bit integers, reductions of large integers by moduli $M$ smaller than $2^{w-1}$ are often implemented sub-optimally, leading applications to take excessive processing time. We present a modular reduction algorithm implementing division by a modulus through multiplication by a reciprocal of that modulus, a well-known method for moduli larger than $2^{w-1}$. We show that application of this method to smaller moduli makes it possible to express certain modular sums and differences without having to compensate for word overflows. By embedding the algorithm in a loop and applying a few transformations to the loop, we obtain an algorithm for reduction of large integers by moduli up to $2^{w-1}$. Implementations of this algorithm can run considerably faster than implementations of similar algorithms that allow for moduli up to $2^w$. This is substantiated by measurements on processors with relatively fast multiplication instructions. It is notoriously hard to specify efficient mathematical algorithms on the level of abstract machine instructions in an error-free manner. In order to eliminate the chance of errors as much as possible, we have created formal correctness proofs of our algorithms, checked by a mechanized proof assistant.

[ PDF ] [ Bibtex ]

Bernard van Gastel, Leonard Lensink, Sjaak Smetsers, and M.C.J.D. van Eekelen. Reentrant Readers-Writers: A Case Study Combining Model Checking and Theorem Proving. Technical report: ICIS-R08005, April, Radboud University Nijmegen, 2008.

The classic readers-writers problem has been extensively studied. This holds to a lesser degree for the reentrant version, where it is allowed to nest locking actions. Such nesting is useful when a library is created with various procedures that each start and end with a lock. Allowing nesting makes it possible for these procedures to call each other. We considered an existing widely used industrial implementation of the reentrant readers-writers problem. We modeled it using a model checker revealing a serious error: a possible deadlock situation. The model was improved and checked satisfactorily for a fixed number of processes. To achieve a correctness result for an arbitrary number of processes the model was converted to a theorem prover with which it was proven.

[ PDF ] [ Bibtex ]

M.A.J. van Gerven, and T. Heskes. L1/Lp regularization of Differences. Technical report: ICIS-R08009, May, Radboud University Nijmegen, 2008.

In this paper, we introduce $L_1/L_p$ regularization of differences as a new regularization approach that can directly regularize models such as the naive Bayes classifier and (autoregressive) hidden Markov models. An algorithm is developed that selects values of the regularization parameter based on a derived stability condition. for the regularized naive Bayes classifier, we show that the method performs comparably to a filtering algorithm based on mutual information for eight datasets that have been selected from the UCI machine learning repository.

[ PDF ] [ Bibtex ]

Perry Groot, T. Heskes, and T.M.H. Dijkstra. Nonlinear perception of hearing-impaired people using preference learning with Gaussian Processes. Technical report: ICIS-R08018, October, Radboud University Nijmegen, 2008.

In this report, we describe a probabilistic kernel approach to pairwise preference learning based on Gaussian Processes and apply the method to audio input signals. The objective is to have a principled approach for modeling and predicting speech quality for arbitrary degradation mechanisms that might be present in a hearing aid. In Arehart et al [2007] pairwise comparisons were performed with 14 normal-hearing and 18 hearing-impaired subjects for several sound distortions. The kernel approach gives a significant improvement in the prediction of sound quality perception over previous results. We show a significant difference between normal-hearing and hearing-impaired subjects, because of nonlinearities in the perception of hearing-impaired subjects.

[ PDF ] [ Bibtex ]

Christian Haack, Marieke Huisman, and Clement Hurlin. Reasoning about Javas Reentrant Locks. Technical report: ICIS-R08014, July, Radboud University Nijmegen, 2008.

This paper presents a verification technique for a concurrent Java-like language with reentrant locks. The verification technique is based on permission-accounting separation logic. As usual, each lock is associated with a resource invariant, when acquiring the lock the resources are obtained by the thread holding the lock, and when releasing the lock, the resources are released. To accommodate for reentrancy, the notion of lockset is introduced: a multiset of locks held by a thread. Keeping track of the lockset enables the logic to ensure that resources are not re-acquired upon reentrancy, thus avoiding the introduction of new resources in the system. To be able to express flexible locking policies, we combine the verification logic with value-parametrized classes. Verified programs satisfy the following properties: data race freedom, absence of null-dereferencing and partial correctness. The verification technique is illustrated on several examples, including a challenging lock-coupling algorithm.

[ PDF ] [ Bibtex ]

T. Heskes, and M.A.J. van Gerven. Stability Conditions for L1/Lp Regularization. Technical report: ICIS-R08002, February, Radboud University Nijmegen, 2008.

This working note derives the stability conditions for L1/Lp regularization.

[ PDF ] [ Bibtex ]

Marieke Huisman, and Erik Poll. Formal Techniques for Java-like Pograms (FTfJP08). Technical report: ICIS-R08013, June, Radboud University Nijmegen, 2008.

This report contains the papers presented at FTfJP08: the 10th workshop on Formal Techniques for Java-like Programs held on July 8th, 2008 in Paphos, Cyprus. This workshop is the tenth in a series of workshops aimed at applying formal techniques to improve modern object-oriented languages. Newer languages such as Java and C# provide good platforms to bridge the gap between formal techniques and practical program development, because of their reasonably clear semantics and standardized libraries. It is our hope that this workshop will encourage the further deployment of well-considered formal techniques.

[ PDF ] [ Bibtex ]

Cezary Kaliszyk, Femke van Raamsdonk, Freek Wiedijk, Hanno Wupper, Maxim Hendriks, and Roel de Vrijer. Deduction using the ProofWeb system. Technical report: ICIS-R08016, September, Radboud University Nijmegen, 2008.

This is the manual of the ProofWeb system that was implemented at the Radboud University Nijmegen and the Free University Amsterdam in the SURF education innovation project Web deduction for education in formal thinking.

[ PDF ] [ Bibtex ]

Pieter Koopman, Rinus Plasmeijer, and Doaitse Swierstra. Draft Proceedings of the Sixth Advanced Functional Programming school (AFP 2008). Technical report: ICIS-R08008, May, Radboud University Nijmegen, 2008.

Draft proceedings of AFP 2008.

[ PDF ] [ Bibtex ]

E Marchiori. Class Conditional Nearest Neighbor and Large Margin Instance Selection. Technical report: ICIS-R08017, October, Radboud University Nijmegen, 2008.

The one nearest neighbor (1-NN) rule uses instance proximity followed by class labeling information for classifying new instances. This paper presents a framework for studying properties of the training set related to proximity and labeling information, in order to improve the performance of the 1-NN rule. To this aim, a so-called class conditional nearest neighbor (c.c.n.n.) relation is introduced, consisting of those pairs of training instances (a, b) such that b is the nearest neighbor of a among those instances (excluded a) in one of the classes of the training set. A graph-based representation of c.c.n.n. is used for a comparative analysis of c.c.n.n. and of other interesting proximity-based concepts. In particular, a scoring function on instances is introduced, which measures the effect of removing one instance on the hypothesis-margin of other instances. This scoring function is employed to develop an effective large margin instance selection algorithm, which is empirically demonstrated to improve storage and accuracy performance of the 1-NN rule on artificial and real-life data sets.

[ PDF ] [ Bibtex ]

J. Nabukenya, P. van Bommel, and H.A. (Erik) Proper. A Theory-Driven Design Approach to Collaborative Policy Making Processes. Technical report: ICIS-R08015, July, Radboud University Nijmegen, 2008.

In this paper, we consider improving collaborative policy making processes. We suggest Collaboration Engineering (CE) as an approach that can be useful in enhancing these processes. However, CE needs a theoretical basis to guide the design. This basis is provided by the quality dimensions and the causal theory. We therefore present a theory that provides an understanding of what makes good policies in policy making. This understanding should lead to design choices that should be taken into account to design quality collaborative policy making processes. To determine the quality dimensions of good policies, we use field exploratory studies and literature in the policy making domain research. Furthermore, we consider cause and effect relationships for these quality dimensions to derive the theory.

[ PDF ] [ Bibtex ]

S.J. Overbeek, P. van Bommel, and H.A. (Erik) Proper. Embedding Knowledge Exchange and Cognitive Matchmaking in a Dichotomy of Markets. Technical report: ICIS-R08003, February, 2008.

Actors require knowledge to improve or gain competencies in order to work successfully. Competencies are improved or gained by executing qualifying tasks. A knowledge market paradigm is introduced to improve the fit between supply and demand of knowledge required by actors performing such qualifying tasks. The eventual work performed by actors can be atomically divided into execution tasks. Discrepancies may exist in the suitability match of actors and the execution tasks that have been allocated to them. Therefore, a knowledge workers market paradigm is introduced as a possible solution to improve the fit between actors and execution tasks.

[ Missing PDF ] [ Bibtex ]

S.J. Overbeek, P. van Bommel, and H.A. (Erik) Proper. Bridging Supply and Demand for Knowledge Intensive Tasks. Technical report: ICIS-R08010, May, 2008.

Two main ingredients related to successful task performance are cognition and quality. Supply and demand of these concepts for knowledge intensive tasks are studied in this paper to fuel successful task fulfillment. Cognitive characteristics are supplied by actors performing tasks. Organizational developments such as growing complexity and increasing customer orientation may increase cognitive load. Stakeholders of tasks have quality requirements. These requirements may be affected if actors experience an increase in cognitive load. It is observed that knowledge intensive tasks demand cognitive characteristics and supply quality factors. Actors supply cognition and stakeholders demand quality. The gap between supply and demand can be bridged by introducing several models. These models consist of a matchmaking framework, conceptual models, and dynamic models. The matchmaking framework shows how supply and demand of cognitive characteristics or quality factors can be matched. Relations and roles of the concepts involved in task fulfillment are mapped out by the conceptual models. The dynamic models show causes that have effects on the supply of cognitive characteristics and the level of quality. These insights in the relations and dependencies between cognition and quality increase our understanding of the key concepts for successful task fulfillment.

[ Missing PDF ] [ Bibtex ]

Rinus Plasmeijer, Sjaak Smetsers, and Arjen van Weelden. Interactive Combining of Typed Object Code. Technical report: ICIS-R08019, November, Radboud University Nijmegen, 2008.

The functional language Clean includes a hybrid type system: in addition to the traditional static type system it offers support for dynamically typed values, so called \emph{dynamics}. An expression of arbitrary static type can be packed into a dynamic, and via pattern matching on types a dynamic can be converted back to a value of statically known type. The most important aspect of dynamics is that they can be serialized, written to file, and exchanged between independently compiled applications in a type-safe way. Since dynamics may contain functions and closures, they can be regarded as type-safe plugins. An application can combine plugins in a type safe way to new ones, without having to know what the actual contents and types of the original plugins are. In this paper we explain the underlying implementation and the architecture of the run-time system needed to make this all possible. To show the expressive power of Cleans dynamics we present an interactive shell, called Esther. The command line language of this shell provides the basic functionality of a strongly typed lazy functional language. Esther behaves like an interpreter (direct response) yet its resulting performance is comparable to compiled code. This is achieved by using the dynamic facility of Clean. The shell actually combines compiled code; no help from a compiler is needed. Moreover, type checking is for free using the run-time type unification of dynamics. In this way we have obtained a novel architectural framework in which one can freely mix functionality created by the compiler, functionality stored in dynamics by compiled applications, and functionality interactively created by using the shell command line interpreter.

[ PDF ] [ Bibtex ]

O. Shkaravska, M. van Eekelen, and A. Tamalet. Collected Size Semantics for Functional Programs over Lists. Technical report: ICIS-R08021, November, 2008.

This work introduces collected size semantics of strict functional programs over lists. The collected size semantics of a function definition is a multivalued size function that collects the dependencies between every possible output size and the corresponding input sizes. Such functions annotate standard types and are defined by conditional rewriting rules generated during type inference. We focus on the connection between the rewriting rules and lower and upper bounds on the multivalued size functions, when the bounds are given by piecewise polynomials. We show how, given a set of conditional rewriting rules, one can infer bounds that define an indexed family of polynomials that approximates the multivalued size function. Using collected size semantics we are able to infer non-monotonic and non-linear lower and upper polynomial bounds for many functional programs. As a feasibility study, we use the procedure to infer lower and upper polynomial size-bounds on typical functions of a list library.

[ PDF ] [ Bibtex ]

O. Shkaravska, M. van Eekelen, and A. Tamalet. Polynomial Size Complexity Analysis with Families of Piecewise Polynomials (with soundness proof and examples in detail). Technical report: ICIS-R08020, November, Radboud University Nijmegen, 2008.

Size analysis can play an important role in optimising memory management and in preventing failure due to memory exhaustion. Static size analysis can be performed using size-aware type systems. In size-aware type systems types express output-on-input size dependencies where sizes of outputs depend on sizes of inputs but they do not depend directly on the actual values. We present a novel type system for a strict functional language. We introduce size annotations that are indexed families of piecewise polynomials. Families are de?ned using indices. They collect possible different size dependencies of a single function. With families compositionality becomes straightforward, even for non-monotonic size dependencies. Lower and upper size bounds can be expressed in a natural way as members of the family. Furthermore, families make it possible to allow non matrix-like structures where inner lists have different lengths. The type system is proven to be sound with respect to a standard operational semantics. Type checking in our type system is not fully decidable. However, we identify two large decidable subclasses. Moreover, the type system admits a semi-automatic inference procedure.

[ PDF ] [ Bibtex ]

Sjaak Smetsers, and Erik Barendsen. Formalizing Type Theory in PVS: a case study. Technical report: ICIS-R08022, December, Radboud University Nijmegen, 2008.

In this case study we investigate the use of PVS for developing type theoretical concepts and verifying the correctness of a typing algorithm. PVS turns out to be very useful for efficient development of a sound basic theory about polymorphic typing. This research contributes to the PoplMark challenge on mechanizing metatheory

[ PDF ] [ Bibtex ]

Alejandro Tamalet, Olha Shkaravska, and Marko van Eekelen. A Size-Aware Type System with Algebraic Data Types. Technical report: ICIS-R08006, April, Radboud University Nijmegen, 2008.

We present a size-aware type system for a first-order functional language with algebraic data types, where types are annotated with polynomials over size variables. We define how to generate typing rules for each data type, provided its user defined size function meets certain requirements. As an example, a program for balancing binary trees is type checked. The type system is shown to be sound with respect to the operational semantics in the class of shapely functions. Type checking is shown to be undecidable, however, decidability for a large subset of programs is guaranteed.

[ PDF ] [ Bibtex ]

Hendrik Tews, Tjark Weber, Marcus VÃ¶lp, Erik Poll, M.C.J.D. van Eekelen, and Peter van Rossum. Nova Micro-Hypervisor Verification. Technical report: ICIS-R08012, May, Radboud University Nijmegen, 2008, Robin deliverable D13.

In this document we describe the work performed in the Robin project towards verifying the Nova micro-hypervisor operating-system kernel. In particular, we describe in detail the Robin verification environment and the results obtained with it. The Robin verification environment consists of the interactive theorem prover PVS, an IA32 (x86) hardware model in PVS, a semantics of (a rich subset of) C++, and a semantics compiler translating C++ sources into their semantics in PVS.

[ PDF ] [ Bibtex ]

H. Tews, Tjark Weber, E. Poll, and M.C.J.D. van Eekelen. Formal Nova interface specification. Technical report: ICIS-R08011, May, 2008, Robin deliverable D12.

This document contains one major result of work package 4 (kernel specification and verification): a formal specification of the Nova interface. The specification consists of three main parts: (1) a definition of an abstract internal state for the Nova micro-hypervisor, (2) a description of the operations of the hypervisor in imperative pseudo-code that accesses and modifies the internal state, and (3) a combination of big-step denotational and small-step operational semantics to give semantics to the pseudo code as state modifying functions.

[ PDF ] [ Bibtex ]

### Professional

S.J. Overbeek, P. van Bommel, and H.A. (Erik) Proper. Systeem voor Cognitieve Afstemming. In: .ego - Magazine voor Informatiekundigen, Nr: 3, Vol: 7, Pages: 19-21, June, 2008, In Dutch.

Dit artikel behandelt een systeem dat de door een werknemer aangeboden cognitieve karakteristieken afstemt op de cognitieve karakteristieken die nodig zijn voor de uitvoering van de dagelijkse taken. Voorbeelden van cognitieve karakteristieken zijn de wilskracht om een taak te vervullen of het bewust zijn van de eisen om een taak af te kunnen ronden. Door middel van cognitieve afstemming kan de meest geschikte werknemer worden gevonden om een bepaalde taak uit te voeren. Wanneer specifiek naar IT organisaties wordt gekeken, zien we dat cognitieve afstemming ondersteuning kan bieden bij systeemontwikkeling. Hoe dit in zijn werk gaat is bestudeerd bij e-office, specialist in digitale werkomgevingen.

[ PDF ] [ Bibtex ]