School of Computing

Publications by Prof Simon Thompson

Also view these in the Kent Academic Repository
Books
Articles

    Thompson, Simon and Laemmel, Ralf and Kaiser, Markus (2013) Programming errors in traversal programs over structured data. Science of Computer Programming. ISSN 0167-6423.

    Abstract

    Traversal strategies à la Stratego (also à la Strafunski and ‘Scrap Your Boilerplate’) provide an exceptionally versatile and uniform means of querying and transforming deeply nested and heterogeneously structured data including terms in functional programming and rewriting, objects in OO programming, and XML documents in XML programming. However, the resulting traversal programs are prone to programming errors. We are specifically concerned with errors that go beyond conservative type errors; examples we examine include divergent traversals, prematurely terminated traversals, and traversals with dead code. Based on an inventory of possible programming errors we explore options of static typing and static analysis so that some categories of errors can be avoided. This exploration generates suggestions for improvements to strategy libraries as well as their underlying programming languages. Haskell is used for illustrations and specifications with sufficient explanations to make the presentation comprehensible to the non-specialist. The overall ideas are language-agnostic and they are summarized accordingly.

    Thompson, Simon and Li, Huiqing (2013) Refactoring tools for functional languages. Journal of Functional Programming, 23 (03). pp. 293-350. ISSN 0956-7968.

    Abstract

    Refactoring is the process of changing the design of a program without changing what it does. Typical refactorings, such as function extraction and generalisation, are intended to make a program more amenable to extension, more comprehensible and so on. Refactorings differ from other sorts of program transformation in being applied to source code, rather than to a ‘core’ language within a compiler, and also in having an effect across a code base, rather than to a single function definition, say. Because of this, there is a need to give automated support to the process. This paper reflects on our experience of building tools to refactor functional programs written in Haskell (HaRe) and Erlang (Wrangler). We begin by discussing what refactoring means for functional programming languages, first in theory, and then in the context of a larger example. Next, we address system design and details of system implementation as well as contrasting the style of refactoring and tooling for Haskell and Erlang. Building both tools led to reflections about what particular refactorings mean, as well as requiring analyses of various kinds, and we discuss both of these. We also discuss various extensions to the core tools, including integrating the tools with test frameworks; facilities for detecting and eliminating code clones; and facilities to make the systems extensible by users. We then reflect on our work by drawing some general conclusions, some of which apply particularly to functional languages, while many others are of general value.

    Boudeville, Olivier and Cesarini, Francesco and Chechina, Natalia et al. (2013) RELEASE: A High-level Paradigm for Reliable Large-scale Server Software. Trends in Functional Programming, 7829.

    Abstract

    Erlang provides a fault-tolerant, reliable model for building concur- rent, distributed system based on functional programming. In the RELEASE pro- ject the Erlang model is extended to Scalable Distributed Erlang – SD Erlang – supporting general-purpose computation in massively multicore systems. This paper outlines the RELEASE proposal, and indicates the progress of the project in its first six months.

    Stapleton, Gem and Taylor, John and Thompson, Simon et al. (2009) The expressiveness of spider diagrams augmented with constants. Journal of Visual Languages and Computing, 20. pp. 30-49.

    Abstract

    Spider diagrams are a visual language for expressing logical statements or constraints. Several sound and complete spider diagram systems have been developed and it has been shown that they are equivalent in expressive power to monadic first order logic with equality. However, these sound and complete spider diagram systems do not contain syntactic elements analogous to constants in first order predicate logic. We extend the spider diagram language to include constant spiders which represent specific individuals. Formal semantics are given for the extended diagram language. We prove that this extended system is equivalent in expressive power to the language of spider diagrams without constants and, hence, equivalent to monadic first order logic with equality.

    Griffin, Darren K. and Mitchell, David and Thompson, Simon (2009) Podcasting by synchronising PowerPoint and voice: What are the pedagogical benefits? Computers and Education, 53 (2). pp. 532-539. ISSN 0360-1315.

    Abstract

    The purpose of this study was to investigate the efficacy of audio-visual synchrony in podcasting and its possible pedagogical benefits. `Synchrony' in this study refers to the simultaneous playback of audio and video data streams, so that the transitions between presentation slides occur at ''lecturer chosen'' points in the audio commentary. Manufacturers of lecture recording software (e.g. ProfCast) would have us believe that the synchrony of image and audio should improve the learning experience. We have yet to see in the literature any empirical evidence to support this hypothesis. In our study, 90 participants in two groups undertook two electronic lectures (e-lectures) on two separate topics, the subject matter of neither was familiar to them beforehand. Each group experienced one ''synchronous'' presentation (e-lecture) of one of the topics, and one ''separate'' presentation (i.e. PowerPoint and audio files separately presented) of the other topic. Each group therefore experienced both ''synchronous'' and ''separate'' delivery and they were then given an MCQ test that assessed five levels of Bloom's taxonomy. Results show no differences in innate ability between the two groups but the evidence supported our primary hypothesis in that statistically significantly higher test scores were seen when participants viewed a synchronous e-lecture; these scores were accounted for by subjects' performance at three of the five levels of Bloom's taxonomy. Qualitative `attitude' survey results also displayed participant preference towards the synchronous over the asynchronous mode of delivery, and in spite of general acceptance of the proposed benefits of electronic proceedings, a majority preference towards traditional rather than electronic lectures. Despite this conservatism, this paper explores in more detail the potential benefits of podcasting via synchronous PowerPoint and voice.

    Li, Huiqing and Thompson, Simon and Reinke, Claus (2005) The Haskell Refactorer, HaRe, and its API. Electronic Notes in Theoretical Computer Science, 141 (4). pp. 29-34. ISSN 1571-0661.

    Stapleton, Gem and Howse, John and Taylor, John et al. (2004) The Expressiveness of Spider Diagrams. Journal of Logic and Computation, 14 (6). pp. 857-880. ISSN 0955-792X.

    Abstract

    Spider diagrams are a visual language for expressing logical statements. In this paper we identify a well-known fragment of first-order predicate logic that we call MFOL=, equivalent in expressive power to the spider diagram language. The language MFOL= is monadic and includes equality but has no constants or function symbols. To show this equivalence, in one direction, for each diagram we construct a sentence in MFOL=, that expresses the same information. For the more challenging converse we prove that there exists a finite set of models for a sentence S that can be used to classify all the models for S. Using these classifying models we show that there is a diagram expressing the same information as S.

    Bowman, Howard and Thompson, Simon (2003) A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection. Journal of Logic and Computation, 13 (2). pp. 195-239. ISSN 0955-792X.

    Abstract

    This paper presents a complete axiomatization for propositional interval temporal logic (PITL) with projection. The axiomatization is based on a tableau decision procedure for the logic, which in turn is founded upon a normal form for PITL formulae. The construction of the axiomatization provides a general mechanism for generating axiomatizations thus: given a normal form for a new connective, axioms can be generated for the connective from the tableau construction using that normal form. The paper concludes with a discussion of aspects of compositionality for PITL with projection.

    Bowman, Howard and Cameron, Helen and King, Peter et al. (2003) Mexitl: Multimedia in Executable Interval Temporal Logic. Formal Methods in System Design, 22 (1). pp. 5-38. ISSN 0925-9856.

    Abstract

    This paper explores a formalism for describing a wide class of multimedia document constraints. The formalism is based on an interval temporal logic. We describe the requirements on temporal logic specification that arise from the multimedia documents application area. In particular, we highlight a canonical specification example. Then we present the temporal logic formalism that we use. This extends existing interval temporal logic with a number of new features: actions, framing of actions, past operators, a projection like operator called filter and a new handling of interval length. A model theory and satisfaction relation is defined for the notation and a specification of the canonical example is presented.

    Cameron, Helen and King, Peter and Thompson, Simon (2003) Modelling Reactive Multimedia: Events and Behaviours. Multimedia Tools and Applications, 19 (1). pp. 53-77. ISSN 1380-7501.

    Abstract

    This paper explores the idea of reactivity in multimedia, and proposes systems which can react to continuously-evolving behaviors as well as to more traditional discrete events. The idea is presented in a scenario as well as in a number of small programming examples. The illustrative examples are written in the Fran system. Fran provides a high-level programming model for animations, built in the Haskell functional programming language. Whilst we use Fran for illustration—and indeed we argue that the functional paradigm is a natural choice of host for such a system—we should stress that the notion of external behaviors within multimedia is independent of the programming environment chosen and could be incorporated into other systems such as SMIL.

    Charles, Nathan and Bowman, Howard and Thompson, Simon (1997) From ACT-ONE to Miranda, a Translation Experiment. Computer Standards and Interfaces, 19 (1). pp. 31-49. ISSN 0920-5489.

    Abstract

    It is now almost universally acknowledged that the data language ACT-ONE associated with the formal description technique LOTOS is inappropriate for the purpose of OSI formal description. In response to this the LOTOS restandardisation activity plans to replace ACT-ONE with a functional language. Thus, compatibility between ACT-ONE and the replacement data language becomes an issue. In response to this, we present an experimental investigation of backward compatibility between ACT-ONE and the new LOTOS data language. Specifically, we investigate translating ACT-ONE data types into the functional language Miranda. Miranda has been chosen as it is a widely used functional programming language and it is close in form to the anticipated new data language. This work serves as a ``verification of concept'' for translating ACT-ONE to the E-LOTOS data language. It identifies the bounds on embedding ACT-ONE in a functional data language. In particular, it indicates what can be translated and what cannot be translated. In addition, the paper reveals pertinent issues which can inform the E-LOTOS work. For example, which constructs are needed in E-LOTOS in order to support the class of data type specifications typically made in the LOTOS setting? We conclude with a number of specific recommendations for the E-LOTOS data language.

    Thompson, Simon (1995) A Logic for Miranda, Revisited. Formal Aspects of Computing (7).

    Abstract

    This paper expands upon work begun in the author's paper 'A Logic for Miranda', Formal Aspects of Computing 1 (1989), in building a logic for the Miranda functional programming language. After summarising the work in that paper, a translation of Miranda definitions into logical formulas is presented, and illustrated by means of examples. This work expands upon the earlier paper in giving a complete treatment of sequences of equations, and by examining how to translate the local definitions introduced by where clauses. The status of the logic is then examined, and it is argued that the logic extends a natural operational semantics of Miranda, given by the translations of definitions into conditional equations. Finally it is shown how the logic can be implemented in the Isabelle proof tool. This paper has been accepted for publication in Formal Aspects of Computing.

    Lins, Rafael D. and Thompson, Simon and Jones, Simon L. Peyton (1994) On the Equivalence Between CMC and TIM. Journal of Functional Programming, 1 (4).

    Abstract

    In this paper we present the equivalence between TIM, a machine developed to implement lazy functional programming languages, and the set of Categorical Multi-Combinators, a rewriting system developed with similar aims. A Complete revision of UKC - Lab.Report 67 (Submitted to Journal of Functional Programming)

    Thompson, Simon and Lins, Rafael D. (1992) The categorical multi-combinator machine - cmcm. Computer Journal, 35 (2). pp. 170-176. ISSN 0010-4620.

    Abstract

    Implementations of functional programming languages can take a number of different forms, and many different machines have been developed for this purpose. This paper introduces another abstract machine, the Categorical Multi-Combinator Machine (CMCM). A thorough introduction to the machines is given, particularly as far as the discussion of the starting of computational information is concerned.

    Thompson, Simon (1989) A Logic for Miranda. Formal Aspects of Computing (1).

Book Sections

    Thompson, Simon (2014) How to stand out digitally. In: Jolly, Adam The Growing Business Handbook. Kogan Page, pp. 129-131. ISBN 9780749470371.

    Abstract

    Professor Simon Thompson, director of research and enterprise at the University of Kent's School of Computing, considers how smaller companies can build a dynamic presence on the web and in social media.

    Thompson, Simon and Howse, John and Taylor, John et al. (2013) On the Completeness of Spider Diagrams Augmented with Constants. In: Moktefi, Amirouche and Shin, Sun-Joo Visual Reasoning with Diagrams. Studies in Universal Logic. Birkhaüser, pp. 101-133. ISBN 9783034805995.

    Abstract

    Diagrammatic reasoning can be described formally by a number of diagrammatic logics; spider diagrams are one of these, and are used for expressing logical statements about set membership and containment. Here, existing work on spider diagrams is extended to include constant spiders that represent specific individuals. We give a formal syntax and semantics for the extended diagram language before introducing a collection of reasoning rules encapsulating logical equivalence and logical consequence. We prove that the resulting logic is sound, complete and decidable.

    Clear, Tony and Caxton, Gwyn and Thompson, Simon et al. (2011) Cooperative and Work-Integrated Education in Information Technology. In: Coll, Richard and Zegwaard, Karsten Integrated Handbook for Cooperative and Work-Integrated Education. World Associate of Cooperative Education, Inc., pp. 182-196. ISBN 978-0-615-51885-5.

    Abstract

    This chapter outlines perspectives on information technology (IT), including definitions of IT, and discusses the way these shape the WIL experience. A continuum model of cooperative education is introduced, followed by an exploration of its components and characteristics through a set of examples and a case study of various hybrid approaches to work-integrated learning in IT. Observing that IT encompasses a diversity of cooperative education models, the chapter concludes with a brief review of issues particular to cooperative education in IT.

    Thompson, Simon (1999) Proof. In: Hammond, Kevin and Michaelson, Greg Research Directions in Parallel Functional Programming. Springer Verlag, pp. 93-119. ISBN 1-85233-092-9.

Conference Items

    Thompson, Simon and Delaney, Aidan and Stapleton, Gem et al. (2014) A Normal Form for Spider Diagrams of Order. In: 2014 International Workshop on Visual Languages and Computing, 27-29 August 2014.

    Abstract

    We develop a reasoning system for an Euler diagram based visual logic, called spider diagrams of order. We de- fine a normal form for spider diagrams of order and provide an algorithm, based on the reasoning system, for producing diagrams in our normal form. Normal forms for visual log- ics have been shown to assist in proving completeness of associated reasoning systems. We wish to use the reasoning system to allow future direct comparison of spider diagrams of order and linear temporal logic.

    Li, Huiqing and Thompson, Simon (2013) Multicore Profiling for Erlang Programs Using Percept2. In: Erlang Workshop 2013, 28 September 2013, Boston, USA.

    Abstract

    Erlang is a functional programming language with built-in support for concurrency based on share-nothing processes and asynchronous message passing. The design of Erlang makes it suitable for writing concurrent and parallel applications, taking full advantage of the computing power of modern multicore machines. However many existing Erlang applications are sequential, in need of parallelisation. In this paper, we present the Erlang concurrency profiling tool Percept2, and demonstrate how the information provided by it can help the user to explore the potential parallelism in an Erlang application and how the system performs on the Erlang multicore system. Percept2 thus allows users improve the performance and scalability of their applications.

    Rodgers, Peter and Baker, Robert and Thompson, Simon et al. (2013) Multi-level Visualization of Concurrent and Distributed Computation in Erlang. In: Visual Languages and Computing (VLC) in The 19th International Conference on Distributed Multimedia Systems (DMS 2013), 8-10 August 2013, Brighton.

    Abstract

    This paper describes a prototype visualization system for concurrent and distributed applications programmed using Erlang, providing two levels of granularity of view. Both visualizations are animated to show the dynamics of aspects of the computation. At the low level, we show the concurrent behaviour of the Erlang schedulers on a single instance of the Erlang virtual machine, which we call an Erlang node. Typically there will be one scheduler per core on a multicore system. Each scheduler maintains a run queue of processes to execute, and we visualize the migration of Erlang concurrent processes from one run queue to another as work is redistributed to fully exploit the hardware. The schedulers are shown as a graph with a circular layout. Next to each scheduler we draw a variable length bar indicating the current size of the run queue for the scheduler. At the high level, we visualize the distributed aspects of the system, showing interactions between Erlang nodes as a dynamic graph drawn with a force model. Speci?cally we show message passing between nodes as edges and lay out nodes according to their current connections. In addition, we also show the grouping of nodes into “s_groups” using an Euler diagram drawn with circles.

    Li, Huiqing and Thompson, Simon (2012) Let's Make Refactoring Tools User-extensible!. In: The Fifth ACM Workshop on Refactoring Tools.

    Abstract

    We present a framework for making a refactoring tool extensible, allowing users to define refactorings from scratch using the concrete syntax of the language, as well as to describe complex refactorings in a domain-specific language for scripting. We demonstrate the approach in practice through a series of examples. The extension framework is built into Wrangler, a tool for refactoring Erlang programs, but we argue that the approach is equally applicable to tools for other languages.

    Moraglio, Alberto and Otero, Fernando E.B. and Johnson, Colin G. et al. (2012) Evolving Recursive Programs using Non-recursive Scaffolding. In: Proceedings of the 2012 IEEE World Congress on Computational Intelligence.

    Abstract

    Genetic programming has proven capable of evolving solutions to a wide variety of problems. However, the successes have largely been with programs without iteration or recursion; evolving recursive programs has turned out to be particularly challenging. The main obstacle to evolving recursive programs seems to be that they are particularly fragile to the application of search operators: a small change in a correct recursive program generally produces a completely wrong program. In this paper, we present a simple and general method that allows us to pass back and forth from a recursive program to an associated non-recursive program. Finding a recursive program can be reduced to evolving non-recursive programs followed by converting the optimum non-recursive program found to the associated optimum recursive program. This avoids the fragility problem above, as evolution does not search the space of recursive programs. We present promising experimental results on a test-bed of recursive problems.

    Li, Huiqing and Thompson, Simon (2012) A Domain-Specific Language for Scripting Refactorings in Erlang. In: 15th Fundamental Approaches to Software Engineering(FASE2012).

    Abstract

    Refactoring is the process of changing the design of a program without changing its behaviour. Many refactoring tools have been developed for various programming languages; their support for composite refactorings â?? refactorings that are composed from a number of primitive refactorings

    Li, Huiqing and Thompson, Simon (2012) Automated API migration in a user-extensible refactoring tool for Erlang programs. In: the 27th IEEE/ACM International Conference on Automated Software Engineering, September 2012, Essen, Germany.

    Abstract

    Wrangler is a refactoring and code inspection tool for Erlang programs. Apart from providing a set of built-in refactorings and code inspection functionalities, Wrangler allows users to define refactorings, code inspections, and general program transformations for themselves to suit their particular needs. These are defined using a template-and rule-based program transformation and analysis framework built into Wrangler.

    Arts, Thomas and Lamela Seijas, Pablo and Thompson, Simon (2011) Extracting QuickCheck Specifications from EUnit Test Cases. In: Erlang Workshop 2011.

    Li, Huiqing and Thompson, Simon and Arts, Thomas (2011) Extracting Properties from Test Cases by Refactoring. In: Proceedings of the Refactoring and Testing Workshop (RefTest 2011).

    Abstract

    A QuickCheck property is a logical statement of aspects of the behaviour of a system. We report on how similar test cases in a test suite written in Erlang can be identified and then refactored into properties, giving a generalisation of the specification implicit in the test suite. Properties give more concise, easier to maintain test suites and better test coverage. A preliminary evaluation of the techniques in industry demonstrates feasibility as well as potential benefits.A QuickCheck property is a logical statement of aspects of the behaviour of a system. We report on how similar test cases in a test suite written in Erlang can be identified and then refactored into properties, giving a generalisation of the specification implicit in the test suite. Properties give more concise, easier to maintain test suites and better test coverage. A preliminary evaluation of the techniques in industry demonstrates feasibility as well as potential benefits

    Li, Huiqing and Thompson, Simon (2011) Incremental Code Clone Detection and Elimination for Erlang Programs. In: Proceedings of the Conference on Fundamental Approaches to Software Engineering (FASE'11).

    Abstract

    A well-known bad code smell in refactoring and software maintenance is the existence of code clones, which are code fragments that are identical or similar to one another. This paper describes an approach to incrementally detecting 'similar' code based on the notion of least-general common abstraction, or anti-unification, as well as a framework for user-controlled incremental elimination of code clones within the context of Erlang programs. The clone detection algorithm proposed in this paper achieves 100 precision, high recall rate, and is user-customisable regarding the granularity of the clone classes reported. By detecting and eliminating clones in an incremental way, we make it possible for the tool to be used in an interactive way even with large codebases. Both the clone detection and elimination functionalities are integrated with Wrangler, a tool for interactive refactoring of Erlang programs. We evaluate the approach with various case studies.

    Cesarini, Francesco and Thompson, Simon (2010) Erlang Behaviours: Programming With Process Design Patterns. In: Central European Functional Programming School, CEFP 2009.

    Abstract

    Erlang processes run independently of each other, each using separate memory and communicating with each other by message passing. These processes, while executing different code, do so following a number of common patterns. By examining different examples of Erlang-style concurrency in client/server architectures, we identify the generic and specific parts of the code and extract the generic code to form a process skeleton. In Erlang, the most commonly used patterns have been implemented in library modules, commonly referred to as OTP behaviours. They contain the generic code framework for concurrency and error handling, simplifying the complexity of concurrent programming and protecting the developer from many common pitfalls.

    Arts, Thomas and Thompson, Simon (2010) From Test Cases to FSMs: Augmented Test-driven Development and Property Inference. In: Erlang'10: Proceedings of the 2010 ACM SIGPLAN Erlang Workshop.

    Abstract

    This paper uses the inference of finite state machines from EUnit test suites for Erlang programs to make two contributions. First, we show that the inferred FSMs provide feedback on the adequacy of the test suite that is developed incrementally during the test-driven development of a system. This is novel because the feedback we give is independent of the implementation of the system. Secondly, we use FSM inference to develop QuickCheck properties for testing state-based systems. This has the effect of transforming a fixed set of tests into a property which can be tested using randomly generated data, substantially widening the coverage and scope of the tests.

    Li, Huiqing and Thompson, Simon (2010) Refactoring Support for Modularity Maintenance in Erlang. In: Tenth IEEE International Working Conference on Source Code Analysis and Manipulation.

    Abstract

    Low coupling between modules and high cohesion inside each module are the key features of good software architecture. Systems written in modern programming languages generally start with some reasonably well-designed module structure; however with continuous feature additions, modifications and bug fixes, software modularity gradually deteriorates; and there is a need for incrementally improving modularity to avoid the situation when the structure of the system becomes too complex to maintain. We demonstrate how Wrangler, a general-purpose refactoring tool for Erlang, could be used to maintain and improve the modularity of programs written in Erlang without dramatically changing the existing module structure. We identify a set of ''modularity smells'' and show how they can be detected by Wrangler and removed by way of a variety of refactorings implemented in Wrangler. Validation of the approach and usefulness of the tool are demonstrated by case studies.

    Li, Huiqing and Thompson, Simon (2010) Improved Testing Through Refactoring: Experience from the ProTest project. In: Testing - Practice and Research Techniques: 5th International Academic and Industrial Conference, TAIC PART 2010.

    Abstract

    We report on how the Wrangler refactoring tool has been used to improve and transform test code for Erlang systems. This has been achieved through the removal of code clones, the identification of properties for property-based testing and the definition of testing-aware refactorings and test-framework-specific refactorings. While some of the observations are Erlang-specific, others apply to test code in general.

    Drienyovszky, Daniel and Horpacsi, Daniel and Thompson, Simon (2010) QuickChecking Refactoring Tools. In: ErlangÂ?10: Proceedings of the 2010 ACM SIGPLAN Erlang Workshop.

    Abstract

    Refactoring is the transformation of program source code in a way that preserves the behaviour of the program. Many tools exist for automating a number of refactoring steps, but these tools are often poorly tested. We present an automated testing framework based on QuickCheck for testing refactoring tools written for the Erlang programming language.

    Delaney, Aidan and Stapleton, Gem and Taylor, John et al. (2010) Fragments of Spider Diagrams of Order and their Relative Expressiveness. In: Diagrammatic Representation and Inference 6th International Conference, Diagrams 2010.

    Abstract

    Investigating the expressiveness of a diagrammatic logic provides insight into how its syntactic elements interact at the semantic level. Moreover, it allows for comparisons with other notations. Various expressiveness results for diagrammatic logics are known, such as the theorem that Shin's Venn-II system is equivalent to monadic first order logic. The techniques employed by Shin for Venn-II were adapted to allow the expressiveness of Euler diagrams to be investigated. We consider the expressiveness of spider diagrams of order (SDoO), which extend spider diagrams by including syntax that provides ordering information between elements. Fragments of SDoO are created by systematically removing each aspect of the syntax. We establish the relative expressiveness of the various fragments. In particular, one result establishes that spiders are syntactic sugar in any fragment that contains order, negation and shading. We also show that shading is syntactic sugar in any fragment containing negation and spiders. The existence of syntactic redundancy within the spider diagram of order logic is unsurprising however, we find it interesting that spiders or shading are redundant in fragments of the logic. Further expressiveness results are presented throughout the paper. The techniques we employ may well extend to related notations, such as the Euler/Venn logic of Swoboda et al. and Kent's constraint diagrams.

    Brown, Christopher and Li, Huiqing and Thompson, Simon (2010) An Expression Processor: A Case Study in Refactoring Haskell Programs. In: Eleventh Symposium on Trends in Functional Programming.

    Abstract

    Refactoring is the process of changing the structure of a program while preserving its behaviour. This behaviour preservation is crucial so that refactorings do not introduce any bugs. Refactoring is aimed at increasing code quality, programming productivity and code reuse. Refactoring has been practised manually by programmers for as long as programs have been written; however, with the advent of refactoring tools, refactoring can be performed semi-automatically, allowing refactorings to be performed (and undone) easily. In this paper, we briefly describe a number of refactorings implemented in the Haskell Refactorer, HaRe. In addition to this, we also implement a simple expression processor to demonstrate how some of the refactorings implemented in HaRe can be used to aid programmers in developing Haskell software.

    Brown, Christopher and Thompson, Simon (2010) Clone Detection and Elimination for Haskell. In: PEPM'10: Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation.

    Abstract

    Duplicated code is a well known problem in software maintenance and refactoring. Code clones tend to increase program size and several studies have shown that duplicated code makes maintenance and code understanding more complex and time consuming. This paper presents a new technique for the detection and removal of duplicated Haskell code. The system is implemented within the refactoring framework of the Haskell Refactorer (HaRe), and uses an Abstract Syntax Tree (AST) based approach. Detection of duplicate code is automatic, while elimination is semi-automatic, with the user managing the clone removal. After presenting the system, an example is given to show how it works in practice.

    Li, Huiqing and Thompson, Simon (2010) Similar Code Detection and Elimination for Erlang Programs. In: Practical Aspects of Declarative languages 2010.

    Abstract

    A well-known bad code smell in refactoring and software maintenance is duplicated code, that is the existence of code clones, which are code fragments that are identical or similar to one another. Unjustified code clones increase code size, make maintenance and comprehension more difficult, and also indicate design problems such as a lack of encapsulation or abstraction. This paper describes an approach to detecting `similar' code based on the notion of anti-unification, or least-general common abstraction. This mechanism is used for detecting code clones in Erlang programs, and is supplemented by a collection of refactorings to support user-controlled automatic clone removal. The similar code detection algorithm and refactorings are integrated within Wrangler, a tool developed at the University of Kent for interactive refactoring of Erlang programs. We conclude with a report on case studies and comparisons with other tools.

    Li, Huiqing and Thompson, Simon (2009) Clone Detection and Removal for Erlang/OTP within a Refactoring Environment. In: ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM'09).

    Abstract

    A well-known bad code smell in refactoring and software maintenance is duplicated code, or code clones. A code clone is a code fragment that is identical or similar to another. Unjustified code clones increase code size, make maintenance and comprehension more difficult, and also indicate design problems such as lack of encapsulation or abstraction. This paper proposes a token and AST based hybrid approach to automatically detecting code clones in Erlang/OTP programs, underlying a collection of refactorings to support user-controlled automatic clone removal, and examines their application in substantial case studies. Both the clone detector and the refactorings are integrated within Wrangler, the refactoring tool developed at Kent for Erlang/OTP.

    Li, Huiqing and Thompson, Simon (2009) Clone Detection and Removal for Erlang/OTP within a Refactoring Environment. In: Third International Workshop on Detection of Software Clones.

    Abstract

    This paper proposes a token and AST based hybrid approach to automatically detecting code clones in Erlang/OTP programs, underlying a collection of refactorings to support user-controlled automatic clone removal. Both the clone detector and the refactorings are integrated within Wrangler, the refactoring tool developed for Erlang/OTP.

    Li, Huiqing and Thompson, Simon (2009) Testing-framework-aware Refactoring. In: The Third ACM Workshop on Refactoring Tools.

    Abstract

    Testing is the predominant way of establishing evidence that a program meets it requirements. When both test code and the application under test are written in the same programming language, a refactoring tool for this language should be able to refactor both application code and testing code together. However, testing frameworks normally come with particular programming idioms, such as their use of naming conventions, coding patterns, meta-programming techniques and the like. A refactoring tool needs to be aware of those programming idioms in order to refactor test code properly. Meanwhile the particularities of test code also suggest refactorings that are particularly applicable to test code. In this paper we present our experience of extending Wrangler, a refactoring tool for the Erlang programming language, so as to handle the three common testing frameworks for Erlang, as well as discussing the refactoring of test code in its own right.

    Li, Huiqing and Thompson, Simon (2008) Tool Support for Refactoring Functional Programs. In: Partial Evaluation and Program Manipulation, CA, Jan 07-08, 2008, San Francisco.

    Abstract

    Tool Support for Refactoring Functional Programs We demonstrate the Haskell Refactorer, HaRe, and the Erlang Refactorer, Wrangler, as examples of fully-functional refactoring tools for functional programming languages. HaRe and Wrangler are designed to handle multi-module projects in complete languages: Haskell 98 and Erlang/OTP. They are embedded in emacs (and gvim) and respect programmer layout styles. In discussing the construction of HaRe and Wrangler, we comment on the different challenges presented by Haskell and Erlang due to their differences in syntax, semantics and pragmatics. In particular, we examine the sorts of analysis that underlie our systems. Finally, drawing on our experience, we examine features common to functional refactorings, and contrast these with refactoring in the object-oriented domain.

    Sultana, Nik and Thompson, Simon (2008) Mechanical Verification of Refactorings. In: Workshop on Partial Evaluation and Program Manipulation, Jan 07-08, 2008, San Francisco, CA,.

    Abstract

    In this paper we describe the formal verification of refactorings for untyped and typed lambda-calculi. This verification is performed in the proof assistant Isabelle/HOL. Refactorings are program transformations applied to improve the design of source code. Well-structured source code is easier and cheaper to maintain, and this motivates the use of refactoring. These transformations have been implemented as programmer tools and, as with other metaprogramming tools, it is desirable that implementations of refactorings are correct. For a refactoring to be correct the refactored program must be identical in behaviour to the original program. Since refactorings are source-to-source transformations, concrete program information matters: for example, names (of variables, procedures, etc) and program layout should also be preserved by refactoring. This is a particular characteristic of refactorings since general program transformations operate over machine representations of programs, rather than readable source code. The paper describes the formalisation adopted, and the alternatives explored. It also reflects on some of the difficulties of performing such formalisations, the interaction between refactoring and phases such as type-checking and parsing, and the generation of correct implementations from mechanised proofs.

    Laemmel, Ralf and Thompson, Simon and Kaiser, Markus (2008) Programming errors in traversal programs over structured data. In: 8th Workshop on Language Description, Tools and Applications.

    Abstract

    Traversal strategies provide an established means of describing automated queries, analyses, transformations, and other non-trivial computations on deeply structured data (including, most notably, data representations of software artifacts such as programs). The resulting traversal programs are prone to programming errors. We are specifically concerned with errors that go beyond classic type errors, in particular: (i) divergence of traversal, (ii) unintentional extent of traversal into data, (iii) trivial traversal results, (iv) inapplicability of the constituents of a traversal program along traversal. We deliver a taxonomy of programming errors, and start attacking some of them by refinements of traversal programming.

    Li, Huiqing and Thompson, Simon (2008) Clone Detection and Removal for Erlang/OTP within a Refactoring Environment. In: Draft Proceedings of the Ninth Symposium on Trends in Functional Programming(TFP).

    Abstract

    A well-known bad code smell in refactoring and software maintenance is duplicated code, or code clones. A code clone is a code fragment that is identical or similar to another. Unjustified code clones increase code size, ake maintenance and comprehension more difficult, and also indicate design problems such as lack of encapsulation or abstraction. This paper proposes a token and AST based hybrid approach to automatically detecting code clones in Erlang/OTP programs, underlying a collection of refactorings to support user-controlled automatic clone removal, and examines their application in substantial case studies. Both the clone detector and the refactorings are integrated within Wrangler, the refactoring tool developed at Kent for Erlang/OTP.

    Sultana, Nik and Thompson, Simon (2008) A Certified Refactoring Engine. In: Draft Proceedings of the Ninth Symposium on Trends in Functional Programming (TFP).

    Abstract

    The paper surveys how software tools such as refactoring systems can be validated, and introduces a new mechanism, namely the extraction of a refactoring engine for a functional programming language from an Isabelle/HOL theory in which it is verified. This research is a first step in a programme to construct certified programming tools from verified theories. We also provide some empirical evidence of how refactoring can be of significant benefit in reshaping automatically-generated program code for use in larger systems.

    Delaney, Aidan and Taylor, John and Thompson, Simon (2008) Spider Diagrams of Order and a Hierarchy of Star-Free Regular Languages. In: Diagrammatic Representation and Inference: 5th International Conference, Diagrams 2008, Herrsching, Germany, September 19-21, 2008, Sep 19-21, 2008, Herrsching, Germany.

    Abstract

    The spider diagram logic forms a fragment of the constraint diagram logic and was designed to be primarily used as a diagrammatic software specification tool. Our interest is in using the logical basis of spider diagrams and the existing known equivalences between certain logics, formal language theory classes and some automata to inform the development of diagrammatic logics. Such developments could have many advantages, one of which would be aiding software engineers who are familiar with formal languages and automata to more intuitively understand diagrammatic logics. In this paper we consider relationships between spider diagrams of order (an extension of spider diagrams) and the star-free subset of regular languages. We extend the concept of the language of a spider diagram to encompass languages over arbitrary alphabets. Furthermore, the product of spider diagrams is introduced. This operator is the diagrammatic analogue of language concatenation. We establish that star-free languages are definable by spider diagrams of order equipped with the product operator and, based on this relationship, spider diagrams of order are as expressive as first order monadic logic of order.

    Li, Huiqing and Thompson, Simon and Orosz, György et al. (2008) Refactoring with Wrangler, updated.

    Abstract

    Wrangler is a refactoring tool for Erlang, implemented in Erlang. This paper reports the latest developments in Wrangler, which include improved user experience. the introduction of a number of data- and process-related refactorings, and also the implementation of an Eclipse plug-in which, together with Erlide, provides refactoring support for Erlang in Eclipse.

    Li, Huiqing and Thompson, Simon and Orosz, George et al. (2008) Refactoring with Wrangler, updated: Data and process refactorings, and integration with Eclipse. In: Proceedings of the Seventh ACM SIGPLAN Erlang Workshop, SEP 27, 2008, Victoria, Canada.

    Abstract

    Wrangler is a refactoring tool for Erlang, implemented in Erlang. This paper reports the latest developments in Wrangler, which include the introduction of a number of data- and process-related refactorings, and also the implementation of an Eclipse plug-in which, together with Erlide, provides refactoring support for Erlang in Eclipse.

    Li, Huiqing and Thompson, Simon (2008) Tool Support for Refactoring Functional Programs. In: Proceedings of the Second ACM SIGPLAN Workshop on Refactoring Tools, Jan 07-08, 2008, San Francisco, CA,.

    Abstract

    We present the Haskell Refactorer, HaRe, and the Erlang Refactorer, Wrangler, as examples of fully-functional refactoring tools for functional programming languages. HaRe and Wrangler are designed to handle multi-module projects in complete languages: Haskell 98 and Erlang/OTP. They are embedded in Emacs, (gVim and Eclipse) and respect programmer layout styles. In discussing the construction of HaRe and Wrangler, we comment on the different challenges presented by Haskell and Erlang due to their differences in syntax, semantics and pragmatics. In particular, we examine the sorts of analysis that underlie our systems.

    Li, Huiqing and Thompson, Simon (2007) Testing Erlang Refactorings with QuickCheck. In: UNSPECIFIED Lecture Notes In Computer Science, 5083. Springer, Freiburg, Germany pp. 19-36. ISBN 978-3-540-85372-5.

    Abstract

    Refactoring is a technique for improving the design of existing programs without changing their behaviour. Wrangler is a tool built at the University of Kent to support Erlang program refactoring; the Wrangler tool is written in Erlang. In this paper we present the use of a novel testing tool, Quviq QuickCheck, for testing the implementation of Wrangler. QuickCheck is a specification-based testing tool for Erlang. With QuickCheck, programs are tested by writing properties in a restricted logic, and using the tool these properties are tested in randomly generated test cases. This paper first gives overviews of Wrangler and Quviq QuickCheck, then discusses the various ways in which refactorings can be validated, and finally shows how QuickCheck can be used to test the correctness of refactorings in an efficient way.

    Brown, Christopher and Thompson, Simon (2007) Refactorings that Split and Merge Programs. In: Draft Proceedings of the 19th International Symposium on Implementation and Application of Functional Languages, IFL 2007, 27th-29th September 2007, Freiburg, Germany.

    Thompson, Simon and King, Peter and Schmitz, Patrick (2007) Declarative extensions of XML languages. In: King, Peter and Simske, Steven ACM Press pp. 89-91. ISBN 978-1-59593-776-6.

    Abstract

    We present a set of XML language extensions that bring notions from functional programming to web authors, extending the power of declarative modelling for the web. Our previous work discussed expressions and user-defined events. In this paper, we discuss how one may extend XML by adding definitions and parameterization; complex data and data types; and reactivity, events and continuous ''behaviours''. We consider these extensions in the light of World Wide Web Consortium standards, and illustrate their utility by a variety of use cases.

    Li, Huiqing and Thompson, Simon and Lövei, László et al. (2006) Refactoring Erlang Programs. In: The Proceedings of 12th International Erlang/OTP User Conference.

    Abstract

    We describe refactoring for Erlang programs, and work in progress to build two tools to give machine support for refactoring systems written in Erlang. We comment on some of the peculiarities of refactoring Erlang programs, and describe in some detail a number of refactorings characteristic of Erlang.

    Li, Huiqing and Thompson, Simon (2006) A Comparative Study of Refactoring Haskell and Erlang Programs. In: Sixth IEEE International Workshop on Source Code Analysis and Manipulation (SCAM 2006), Sep 27-29, 2006, Philadelphia, PA,.

    Abstract

    Refactoring is about changing the design of existing code without changing its behaviour, but with the aim of making code easier to understand, modify, or reuse. Taking Haskell and Erlang as examples, we investigate the application of refactoring techniques to functional programs, and building tools for supporting interactive refactoring. Although both Haskell and Erlang are general-purpose functional programming languages, they have many differences in their language design and programming idioms. As a result, program refactoring in the two languages has much in common, but also considerable differences. This paper makes this comparison, and in particular looks in more detail at the refactorings applicable in each language, the program analysis required by typical refactorings, and at tool support for refactoring Haskell and Erlang programs.

    Patrascoiu, Octavian and Thompson, Simon and Rodgers, Peter (2005) Tableaux for Diagrammatic Reasoning. In: Proceedings of the 2005 International Workshop on Visual Languages and Computing.

    Abstract

    Diagrammatic notations, such as the Unified Modeling Language (UML), are in common use in software development. They allow many aspects of software systems to be described diagrammatically, but typically they rely on textual notations for logical constraints. In contrast, spider diagrams provide a visual notation for expressing a natural class of set- theoretic statements in a diagrammatic form. In this paper we present a tableau system for spider diagrams, and describe an implementation of the system. In a software development context, the system allows users to explore the implications of design choices, and thus to validate specifications; beyond this, the tableau algorithm and system are of general interest to visual reasoners.

    Stapleton, Gem and Thompson, Simon and Fish, Andrew et al. (2005) A New Language for the Visualization of Logic and reasoning. In: Proceedings of the 2005 International Workshop on Visual Languages and Computing.

    Abstract

    Many visual languages based on Euler diagrams have emerged for expressing relationships between sets. The expressive power of these languages varies, but the majority can only express statements involving unary relations and, sometimes, equality. We present a new visual language called Visual First Order Logic (VFOL) that was developed from work on constraint diagrams which are designed for software specification. VFOL is likely to be useful for software specification, because it is similar to constraint diagrams, and may also fit into a Z-like framework. We show that for every First Order Predicate Logic (FOPL) formula there exists a semantically equivalent VFOL diagram. The translation we give from FOPL to VFOL is natural and, as such, VFOL could also be used to teach FOPL, for example.

    Ryder, Chris and Thompson, Simon (2005) Software Metrics: Measuring Haskell.

    Abstract

    Software metrics have been used in software engineering as a mechanism for assessing code quality and for targeting software development activities, such as testing or refactoring, at areas of a program that will most benefit from them. Haskell has many tools for software engineering, such as testing, debugging and refactoring tools, but software metrics have mostly been neglected. The work presented in this paper identifies a collection of software metrics for use with Haskell programs. These metrics are subjected to statistical analysis to assess the correlation between their values and the number of bug fixing changes occurring during the development lifetime of two case study programs. In addition to this, the relationships between the metric values is also explored, showing how combinations of metrics can be used to improve the accuracy of the measurements.

    Li, Huiqing and Thompson, Simon (2005) Formalisation of Haskell Refactorings. In: van Eekelen, Marko and Hammond, Kevin ISBN 9781841501765.

    Abstract

    Refactoring is a well-known technique for improving the design of existing programs without changing their external behaviour. HaRe is the refactoring tool we have built to support refactoring Haskell programs. Along with the development of HaRe, This formalisation process helps to clarify the meaning of refactorings, improves our confidence in the behaviour-preservation of refactorings, and reduces the need for testing. This paper gives an overview of HaRe, and shows our approach to the formalisation of refactorings.

    Stapleton, Gem and Howse, John and Taylor, John et al. (2004) The Expressiveness of Spider Diagrams Augmented with Constants. In: UNSPECIFIED IEEE pp. 90-98. ISBN 0-7803-8696-5.

    Abstract

    Spider diagrams are a visual language for expressing logical statements. Spiders represent the existence of elements and contours denote sets. Several sound and complete spider diagram systems have been developed and it is known that the spider diagram language is equivalent in expressive power to monadic first order logic with equality. However, these sound and complete spider diagram systems do not contain syntactic elements analogous to constants in first order predicate logic. We extend the spider diagram language to include constant spiders which represent specific individuals and give formal semantics for the extended diagram language. We then prove that this extended system is equivalent in expressive power to the language of spider diagrams without constants.

    Stapleton, Gem and Howse, John and Taylor, John et al. (2004) What Can Spider Diagrams Say? In: Blackwell, Alan and Marriott, Kim and Shimojima, Atsushi Lecture Notes in Computer Science, 2980. Springer pp. 179-186. ISBN 3-540-21268-X.

    Abstract

    Spider diagrams are a visual notation for expressing logical statements. In this paper we identify a well known fragment of first order predicate logic, that we call ESD, equivalent in expressive power to the spider diagram language. The language ESD is monadic and includes equality but has no constants or function symbols. To show this equivalence, in one direction, for each diagram we construct a sentence in ESD that expresses the same information. For the more challenging converse we show there exists a finite set of models for a sentence S that can be used to classify all the models for S. Using these classifying models we show that there is a diagram expressing the same information as S.

    King, Peter and Schmitz, Patrick and Thompson, Simon (2004) Behavioural Reactivity and Real Time Programming in XML: Functional Programming meets SMIL animation. In: Vion-Dury, Jean-Yves ACM New York, NY, USA pp. 57-66. ISBN 1-58113-938-1.

    Abstract

    XML and its associated languages are emerging as powerful authoring tools for multimedia and hypermedia web content. Furthermore, intelligent presentation generation engines have begun to appear, as have models and platforms for adaptive presentations. However, XML-based models are limited by their lack of expressiveness in presentation and animation. As a result, authors of dynamic, adaptive web content must often use considerable amounts of script or code. The use of such script or code has two serious drawbacks. First, such code undermines the declarative description possible in the original presentation language, and second, the scripting/coding approach does not readily lend itself to authoring by non-programmers. In this paper we describe a set of XML language extensions, inspired by features from the functional programming world, which are designed to widen the class of reactive systems which could be described in languages such as SMIL. The features which we discuss extend the power of declarative modeling for the web by allowing the introduction of web media items which may dynamically react to continuously varying inputs, both in a continuous way and by triggering discrete, user-defined, events. The two extensions described herein are discussed in the context of SMIL Animation and SVG, but could be applied to many XML-based languages.

    Thompson, Simon (2004) Refactoring Functional Programs. In: Advanced Functional Programming: 5th International School, AFP 2004, August 14-21, 2004, Estonia.

    Abstract

    Refactoring is the process of improving the design of existing programs without changing their functionality. These notes cover refactoring in functional languages, using Haskell as the medium, and introducing the HaRe tool for refactoring in Haskell.

    Li, Huiqing and Reinke, Claus and Thompson, Simon (2003) Tool Support for Refactoring Functional Programs. In: ACM SIGPLAN 2003 Haskell Workshop.

    Abstract

    Refactorings are source-to-source program transformations which change program structure and organisation, but not program functionality. Documented in catalogues and supported by tools, refactoring provides the means to adapt and improve the design of existing code, and has thus enabled the trend towards modern agile software development processes. Refactoring has taken a prominent place in software development and maintenance, but most of this recent success has taken place in the OO and XP communities. In our project, we explore the prospects for Refactoring Functional Programs, taking Haskell as a concrete case-study. This paper discusses the variety of pragmatic and implementation issues raised by our work on the Haskell Refactorer. We briefly introduce the ideas behind refactoring, and a set of elementary functional refactorings. The core of the paper then outlines the main challenges that arise from our aim to produce practical tools for a decidedly non-toy language, summarizes our experience in trying to establish the necessary meta-programming infrastructure and gives an implementation overview of our current prototype refactoring tool. Using Haskell as our implementation language, we also offer some preliminary comments on Haskell programming-in-the-large.

    Thompson, Simon and Reinke, Claus (2003) A Case Study in Refactoring Functional Programs. In: VII Brazilian Symposium on Programming Languages, May 2003.

    Abstract

    Refactoring is the process of redesigning existing code without changing its functionality. Refactoring has recently come to prominence in the OO community. In this paper we explore the prospects for refactoring functional programs. Our paper centres on the case study of refactoring a 400 line Haskell program written by one of our students. The case study illustrates the type and variety of program manipulations involved in refactoring. Similarly to other program transformations, refactorings are based on program equivalences, and thus ultimately on language semantics. In the context of functional languages, refactorings can be based on existing theory and program analyses. However, the use of program transformations for program restructuring emphasises a different kind of transformation from the more traditional derivation or optimisation: characteristically, they often require wholesale changes to a collection of modules, and although they are best controlled by programmers, their application may require nontrivial semantic analyses. The paper also explores the background to refactoring, provides a taxonomy for describing refactorings and draws some conclusions about refactoring for functional programs.

    Schmitz, Patrick and Thompson, Simon and King, Peter (2003) Presentation Dynamism in XML.

    Abstract

    The move towards a semantic web will produce an increasing number of presentations whose creation is based upon semantic queries. Intelligent presentation generation engines have already begun to appear, as have models and platforms for adaptive presentations. However, in many cases these models are constrained by the lack of expressiveness in current generation presentation and animation languages. Moreover, authors of dynamic, adaptive web content must often use considerable amounts of script or code, thus breaking the declarative description possible in the original presentation language. Furthermore, the scripting/coding approach does not lend itself to authoring by non-programmers. In this paper we describe a set of XML language extensions that bring tools from the functional programming world to web authors, extending the power of declarative modeling for the web. The extensions are described in the context of SMIL Animation and SVG, but could be applied to many XML-based languages.

    Hanus, Michael and Krishnamurthy, Shriram and Thompson, Simon (2002) Functional and Declarative Programming in Education 2002. In: Functional and Declarative Programming in Education (FDPE02), Monday 7 October 2002, Pittsburgh, PA, USA.

    Abstract

    This report contains the proceedings of the International Workshop on Functional and Declarative Programming in Education (FDPE 2002), held in Pittsburgh (USA) on October 7, 2002 as part pf PLI 2002 (Principles, Logics, and Implementations of high-level programming languages). Functional and declarative programming plays an increasingly important role in computing education at all levels. This workshop aimed at bringing together educators and others who are interested in exchanging ideas on how to use a functional or declarative programming style in the classroom. Previous workshops have been held in Paris (1999) and Southampton (1997). The technical program of the workshop included standard presentations as well as short talks or "tricks of the trade" presentations focusing on small but neat ides. The organizers reviewed all papers submitted in response to a call for papers. Following the review process and a lively email discussion, the organizers selected the papers contained in these proceedings for presentation at the workshop. The organizers would like to thank the organization team of PLI 2002 for hosting the workshop and Klaus Höppner for his help in the preparation of the proceedings.

    Thompson, Simon (2001) Logic and Dependent Types in the Aldor Computer Algebra System. In: Symbolic Computation and Automated Reasoning, Aug 06-07, 2000, St Andrews, Scotland.

    Abstract

    We show how the Aldor type system can represent propositions of first-order logic, by means of the 'propositions as types' correspondence. The representation relies on type casts (using pretend) but can be viewed as a prototype implementation of a modified type system with type evaluation reported elsewhere [9]. The logic is used to provide an, axiomatisation of a number of familiar Aldor categories as well as a type of vectors

    Poll, Erik and Thompson, Simon (2000) Integrating Computer Algebra and Reasoning through the Type System of Aldor. In: 3rd International Workshop on Frontiers of Combining Systems (FroCoS 2000), MAR 22-24, 2000, Nancy, France.

    Abstract

    A number of combinations of reasoning and computer algebra systems have been proposed; in this paper we describe another, namely a way to incorporate a logic in the computer algebra system Axiom. We examine the type system of Alder - the Axiom Library Compiler and show that with some modifications we can use the dependent types of the system to model a logic, under the Curry-Howard isomorphism. We give a number of example applications of the logic we construct and explain a prototype implementation of a modified type-checking system written in Haskell.

    Cameron, Helen and King, Peter and Bowman, Howard et al. (1998) Synchronization in Multimedia Documents. In: Andre, Jacques Lecture Notes In Computer Science, 1357. Springer pp. 355-369. ISBN 3-540-64298-6.

    Abstract

    This paper presents a taxonomy of possible synchronization relationships between pairs of items in multimedia documents. Several existing approaches to the synchronization of entire items are reviewed. We then discuss classes of synchronization based upon dynamic events or conditions occurring within media items and their internal structure. We present a taxonomy of seventy-two possible such relations, which are illustrated by numerous examples and which are formalized in the authors' temporal logic notation, Mexitl. The ideas are then applied to provide a description of the lip-synchronization problem.

    Bowman, Howard and Thompson, Simon (1998) A Tableaux Method for Interval Temporal Logic with Projection. In: UNSPECIFIED Lecture Notes In Computer Science, 1397 (1397). Springer-Verlag pp. 108-123. ISBN 3-540-64406-7.

    Abstract

    Tableau Methods have been extensively investigated for standard (infinite) temporal logics and there has been some tableau work in the interval temporal logic setting. However, this work has not considered the important projection operator. This paper responds to this deficiency by defining just such a tableau algorithm which handles the projection operator.

    Thompson, Simon (1997) em Where do I begin? A problem solving approach to teaching functional programming. In: First International Conference on Declarative Programming Languages in Education.

    Abstract

    This paper introduces a problem solving method for teaching functional programming, based on Polya's `How To Solve It', an introductory investigation of mathematical method. We first present the language independent version, and then show in particular how it applies to the development of programs in Haskell. The method is illustrated by a sequence of examples and a larger case study.

    Barnes, David J. and Fincher, Sally and Thompson, Simon (1997) Introductory Problem Solving in Computer Science. In: 5th Annual Conference on the Teaching of Computing.

    Abstract

    This paper describes our experiences in devising a lightweight, informal methodology for problem solving in introductory, university level, computer science. We first describe the original context of the experiment and the background to the methodology. We then give the details of the steps of the Problem Solving Cycle - Understanding, Designing, Writing and Reviewing - and the lessons we learned about our teaching from devising the material. We also present practical examples of how it has been applied in a variety of units in our programme.

    Bowman, Howard and Cameron, Helen and King, Peter et al. (1997) Specification and Prototyping of Structured Multimedia Documents using Interval Temporal Logic. In: International Conference on Temporal Logic.

    Abstract

    This paper explores a formalism for describing a wide class of multimedia document constraints. The formalism is based on an interval temporal logic. We describe the requirements on temporal logic specification that arise from the multimedia documents application area. In particular, we highlight a canonical document example. Then we present the temporal logic formalism that we use. This formalism extends existing interval temporal logic with a number of new features: actions, framing of actions, past operators, a projection-like operator called filter and a new handling of interval length. A model theory and satisfaction relation is defined for the notation and a specification of the canonical example is presented.

    Thompson, Simon (1997) Constructive interval temporal logic in Alf. In: Barringer, Howard Applied Logic. Kluwer pp. 377-390.

    Abstract

    This paper gives an implementation of an interval temporal logic in a constructive type theory, using the Alf proof system. After explaining the constructive approach, its relevance to interval temporal logic and potential applications of our work, we explain the fundamentals of the Alf system. We then present the implementation of the logic and give a number of examples of its use. We conclude by exploring how the work can be extended in the future.

    Thompson, Simon and Hill, Steve (1995) Functional programming through the curriculum. In: 1st International Symposium on Functional Programming Languages in Education (FPLE 95), Dec 04-06, 1995, Nijmegen, Netherlands.

    Abstract

    This paper discusses our experience in using a functional language in topics across the computer science curriculum. After examining the arguments for taking a functional approach, we look in detail at four case studies from different areas: programming language semantics, machine architectures, graphics and formal languages.

    Hill, Steve and Thompson, Simon (1995) Miranda in Isabelle. In: Preceedings of the first Isabelle Users Workshop.

    Abstract

    This paper describes our experience in formalising arguments about the Miranda functional programming language in Isabelle. After explaining some of the problems of reasoning about Miranda, we explain our two different approaches to encoding Miranda in Isabelle. We conclude by discussing some shorter examples and a case study of reasoning about hardware.

    Abstract

    After introducing Martin-Lof's type theory, the paper introduces the rules proposed by various authors for adding subset types to the system, and the justification given for their addition. These justifications are examined, and it is argued that by a combination of lazy evaluation and transformation using the Axiom of Choice that subsets need not be added to the system to make it usable.

Monographs

    Lamela Seijas, Pablo and Thompson, Simon and Taylor, Ramsay et al. (2014) Synapse: automatic behaviour inference and implementation comparison for Erlang. technical_report. University of Kent (unpublished)

    Abstract

    In the open environment of the world wide web, it is natural that there will be multiple providers of services, and that these service provisions — both specifications and implementations — will evolve. This multiplicity gives the user of these services a set of questions about how to choose between different providers, as well as how these choices work in an evolving environment. The challenge, therefore, is to concisely represent to the user the behaviour of a particular implementation, and the differences between this implementation and alternative versions. Inferred models of software behaviour – and automatically derived and graphically presented comparisons between them – serve to support effective decision making in situations where there are competing implementations of requirements. In this paper we use state machine models as the abstract representation of the behaviour of an implementation, and using these we build a tool by which one can visualise in an intuitive manner both the initial implementation and the differences between alternative versions. In this paper we describe our tool Synapse which implements this functionality by means of our grammar inference tool StateChum and a model-differencing algorithm. We describe the main functionality of Synapse, and demonstrate its usage by comparing different implementations of an example program from the existing literature.

    Lamela Seijas, Pablo and Li, Huiqing and Thompson, Simon (2013) Towards Property-Based Testing of RESTful Web Services. technical_report. School of Computing, University of Kent (unpublished)

    Abstract

    Developing APIs as Web Services over HTTP implies adding an extra layer to software, compared to the ones that we would need to develop an API distributed as, for example, a library. This additional layer must be included in testing too, but this implies that the software under test has an additional complexity due both to the need to use an intermediate protocol in tests and to the need to test compliance with the constraints imposed by that protocol: in this case the constraints defined by the REST architectural style. On the other hand, these requirements are common to all the Web Services, and because of that, we should be able to abstract this aspect of the testing model so that we can reuse it in testing any Web Service. In this paper, as a first step towards automating the testing of Web Services over HTTP, we describe a practical mechanism and model for testing RESTful Web Services without side effects and give an example of how we successfully adapted that mechanism to test two different existing Web Services: Storage Room by Thriventures and Google Tasks by Google. For this task we have used Erlang together with state machine models in the property-based testing tool Quviq QuickCheck, implemented using the statem module.

    Li, Huiqing and Thompson, Simon (2011) A User-extensible Refactoring Tool for Erlang Programs. technical_report.

    Abstract

    Refactoring is the process of changing the design of a program without changing what it does. While it is possible to refactor a program by hand, tool support is considered invaluable as it allows large-scale refactorings to be performed easily. However, most refactoring tools are black boxes, supporting a fixed set of `core' refactorings. This paper reports the framework built into Wrangler â?? a refactoring and code inspection tool for Erlang programs

    Li, Huiqing and Thompson, Simon (2011) A Domain-Specific Language for Scripting Refactorings in Erlang. technical_report.

    Abstract

    Refactoring is the process changing the design of a program without changing its behaviour. Many refactoring tools have been developed for various programming languages; while these told support primitive, atomic refactorings, support for composite refactorings â?? refactorings that are composed from a number of primitive refactorings

    Li, Huiqing and Lindberg, Adam and Schumacher, Andreas et al. (2009) Improving your test code with Wrangler. technical_report.

    Abstract

    In this paper we show how the 'similar code' detection facilities of Wrangler, combined with its portfolio of refactorings, allow test code to be shrunk dramatically, under the guidance of the test engineer. This is illustrated by a sequence of refactorings of a test suite taken from an Erlang project at Ericsson AB.

    Thompson, Simon and King, Peter (2007) Declarative Extensions of XML Languages. technical_report. University of Kent, Canterbury, Kent

    Abstract

    This work is a continuation of previous, published joint work towards a set of XML language extensions that bring tools from the functional programming world to web authors, extending the power of declarative modeling for the web. Our previous work concentrated on two aspects, expressions and user-defined events, and deliberately left aside other questions regarding data types, encapsulation and so forth. Work addressed here includes the addition of various facilities to XML languages including definitions and parameterization; complex data and data types; reactivity, events and continuous ''behaviours''. We have considered these extensions in the light of existing and emerging World Wide Web Consortium standards.

    Ryder, Chris and Thompson, Simon (2005) Porting HaRe to the GHC API. technical_report. Computing Laboratory, University of Kent, University of Kent, Canterbury, Kent, UK

    Li, Huiqing and Reinke, Claus and Thompson, Simon (2004) Progress on HaRe: the Haskell Refactorer. other. kent university (unpublished)

    Thompson, Simon and Reinke, Claus (2001) Refactoring Functional Programs. technical_report. Computing Laboratory, University of Kent, Canterbury, Kent

    Abstract

    Refactoring is the process of redesigning existing code without changing its functionality. Refactoring has recently come to prominence in the OO community. In this paper we explore the prospects for refactoring functional programs. Our paper centres on the case study of refactoring a 400 line Haskell program written by one of our students. The case study illustrates the type and variety of program manipulations involved in refactoring. Similarly to other program transformations, refactorings are based on program equivalences, and thus ultimately on language semantics. In the context of functional languages, refactorings can be based on existing theory and program analyses. However, the use of program transformations for program restructuring emphasises a different kind of transformation from the more traditional derivation or optimisation: characteristically, they often require wholesale changes to a collection of modules, and although they are best controlled by programmers, their application may require nontrivial semantic analyses. The paper also explores the background to refactoring, provides a taxonomy for describing refactorings and draws some conclusions about refactoring for functional programs.

    Bowman, Howard and Thompson, Simon (2000) A Complete Axiomatization of Interval Temporal Logic with Projection. technical_report. University of Kent

    Abstract

    This paper presents a complete axiomatisation for propositional interval temporal logic (PITL) with projection. The axiomatisation is based on a tableau procedure for the logic, which in turn is founded upon a normal form for PITL formluae. The construction of the axiomatisation is modular, in the sense that given a normal form for a new connective, axioms can be generated for the connective from the tableau construction. The paper concludes with a discussion of aspects of compositionality for PITL with projection.

    Thompson, Simon (2000) Regular Expressions and Automata using Haskell. technical_report. University of Kent

    Abstract

    The paper begins with definitions of regular expressions, and how strings are matched to them; this also gives our first Haskell treatment also. After describing the abstract data type of sets we define non-deterministic finite automata, and their implementation in Haskell. We then show how to build an NFA corresponding to each regular expression, and how such a machine can be optimised, first by transforming it into a deterministic machine, and then by minimising the state space of the DFA. We conclude with a discussion of regular definitions, and show how recognisers for strings matching regular definitions can be built.

    Ryder, Chris and Thompson, Simon (1999) Aldor meets Haskell. technical_report. Computing Laboratory, University of Kent

    Abstract

    As part of a project to include reasoning capabilities in the Aldor computer algebra system it is necessary to modify the type checking algorithm in Aldor. This paper reports on work to write Aldor abstract syntax trees as elements of Haskell data types, and to implement a prototype modified type checker for Aldor in Haskell.

    Felleisen, Matthias and Hanus, Michael and Thompson, Simon (1999) Proceedings of the 1999 Workshop on Functional and Declarative Programming in Education. technical_report. Rice University

    Poll, Erik and Thompson, Simon (1999) The Type System of Aldor. technical_report., Kent CT2 7NF, UK

    Abstract

    This paper gives a formal description of (at least a part of) the type system of Aldor, the extension language of the computer algebra system AXIOM. In the process of doing this a critique of the design of the system emerges.

    Poll, Erik and Thompson, Simon (1998) Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor. technical_report. Kent University

    Abstract

    A number of combinations of theorem proving and computer algebra systems have been proposed; in this paper we describe another, namely a way to incorporate a logic in the computer algebra system Axiom. We examine the type system of Aldor -- the Axiom Library Compiler -- and show that with some modifications we can use the dependent types of the system to model a logic, under the Curry-Howard isomorphism. We give a number of example applications of the logic we construct.

    Thompson, Simon (1998) A Functional Reactive Animation of a Lift using Fran. technical_report. Cambridge University Press

    Abstract

    This paper uses the Functional Reactive Animation system, Fran, to give a simulation of a simple two floor lift (or elevator). We introduce those aspects of Fran relevant to the simulation, thus making the paper self-contained. We show how to extend the design to one for a lift with an arbitrary number of floors, and we conclude the paper with a discussion of how the Fran simulation can be verified in an informal temporal logic.

    Bowman, Howard and Thompson, Simon (1997) A Tableau Method for Interval Temporal Logic. technical_report. University of Kent at Canterbury

    Abstract

    In this paper we present a complete tableau method for interval temporal logic including the projection operator. Central to our strategy is the identification of normal forms for all the operators of our logic. In effect, these normal forms give inductive definitions of the ITL operators. Then, in the style of Wolper, we define a tableau decision procedure to check satisfiability of our logic. For simplicity of presentation we work in the propositional setting.

    Bowman, Howard and Cameron, Helen and King, Peter et al. (1997) Mexitl: Multimedia in Executable Interval Temporal Logic. technical_report. University of Kent

    Abstract

    This paper explores a formalism for describing a wide class of multimedia document constraints, based on an interval temporal logic. We describe the requirements on temporal logic specification that arise from the multimedia documents application area. In particular, we highlight a canonical specification example. Then we present the temporal logic formalism that we use. This extends existing interval temporal logic with a number of new features: actions, framing of actions, past operators, a projection-like operator called filter and a new handling of interval length. A model theory, logic and satisfaction relation are defined for the notation, a specification of the canonical example is presented, and a proof system for the logic is introduced.

    Thompson, Simon (1997) Higher-order + Polymorphic = Reusable. other. University of Kent (unpublished)

    Abstract

    This paper explores how certain ideas in object oriented languages have their correspondents in functional languages. In particular we look at the analogue of the iterators of the C++ standard template library. We also give an example of the use of constructor classes which feature in Haskell 1.3 and Gofer.

    Telford, Alastair J. and Thompson, Simon (1996) Abstract Interpretation of Constructive Type Theory. technical_report. UKC, University of Kent, Canterbury, UK

    Abstract

    Constructive type theories, such as that of Martin-Lof, allow program construction and verification to take place within a single system: proofs may be read as programs and propositions as types. However, parts of proofs may be seen to be irrelevant from a computational viewpoint. We show how a form of abstract interpretation may be used to detect computational redundancy in a functional language based upon Martin-Lof's type theory. Thus, without making any alteration to the system of type theory itself, we present an automatic way of discovering and removing such redundancy. We also note that the strong normalisation property of type theory means that proofs of correctness of the abstract interpretation are simpler, being based upon a set-theoretic rather than a domain-theoretic semantics. Keywords: Type theory, functional programming, computational redundancy, abstract interpretation.

    Thompson, Simon (1995) Programming Language Semantics using Miranda. technical_report. UKC, University of Kent, Canterbury, UK

    Abstract

    This paper explains the use of the functional programming language Miranda as a vehicle for describing the semantics of imperative programming languages. In particular we give a Miranda denotational description of a substantial subset of a Pascal-like language, describing a number of variants of the semantics, including parameter passing by value-result, dynamic binding of values to names and a simple semantics of jumps. We also give an executable operational semantics of our basic language, as well as a compiler for this language into a simple stack machine, which is itself modelled in Miranda.

    Thompson, Simon (1995) Regular Expressions and Automata using Miranda. other. UKC (unpublished)

    Abstract

    In these notes Miranda is used as a vehicle to introduce regular expressions, pattern matching, and their implementations by means of non-deterministic and deterministic automata. As part of the material, we give an implementation of the ideas, contained in a set of files. References to this material are scattered through the text. The files can be obtained by following the instructions in medskip noindent tt http://www.ukc.ac.uk/computer_science/Miranda_craft/regExp.html medskip noindent This material is based on the treatment of the subject in `the Dragon book', but provides full implementations rather than their pseudo-code versions of the algorithms. The material gives an illustration of many of the features of Miranda, including polymorphism (the states of an NFA can be represented by objects of any type); modularisation (the system is split across a number of modules); higher-order functions (used in finding limits of processes, for example) and other features.

    Thompson, Simon (1992) Formulating Haskell. technical_report. University of Kent, Canterbury, UK

    Abstract

    The functional programming language Haskell is examined from the point of view of proving programs correct. Particular features explored include the data type definition facilities, classes, the behaviour of patterns and guards and the monad approach to IO in the Glasgow Haskell compiler.

    Lins, Rafael D. and Thompson, Simon (1990) Implementing SASL using Categorical Multi-combinators. technical_report. UKC, University of Kent, Canterbury, UK

    Thompson, Simon (1987) Interactive Functional Programs: a Method and a Formal Semantics. technical_report. Computing Laboratory, University of Kent, Canterbury, UK

    Abstract

    In this paper we present a model of interactive programs in a purely functional style. We exploit lazy evaluation in the modelling of streams as lazy lists. We show how programs may be constructed in an ad hoc way, and then present a small set of interactions and combinators which form the basis for a disciplined approach to writing such programs. One of the difficulties of the ad hoc approach is that the way in which input and output are interleaved by the functions can be unpredictable. In the second half of the paper we use traces, i.e. partial histories of behaviour, to explain the interleaving of input and output, and give a formal explanation of our combinators. We argue that this justifies our claim that the combinators have the intuitively expected behaviour, and finally contrast our approach with another.

    Thompson, Simon (1986) Proving properties of functions defined on lawful types. technical_report. Computing Laboratory, University of Kent, University of Kent, Canterbury, UK

Other
Total publications in KAR: 113 [See all in KAR]

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 24/10/2014