LtU Forum

Strengthening Process Calculi

Mingsheng Ying: Topology in process calculus: approximate correctness and infinite evolution of concurrent programs.

Since process calculi come up now and then, I borrowed this book from the library and tried to read it. Cannot claim to have grokked it, but I was excited reading through the example applications toward the end of it. I (think I) am hoping this kind of work can find its way into the main-stream somehow, some day.

Communication and concurrency are essential in understanding complex dynamic systems, and there have been many theories to deal with them such as Petri nets, CSP and ACP. Among them, process calculus is one of the most important and mathematically developed models of communication and concurrency. Various behavior equivalences between agents, such as (strong and weak) bisimilarity, observation congruence, trace equivalence, testing equivalence and failure equivalence, are central notions in process calculus.

In the real applications of process calculus, specification and implementation are described as two agents, correctness of programs is treated as a certain behavior equivalence between specification and implementation, and then the proof of correctness of programs is a task to establish some behavior equivalence between them.

The goal of this book is to provide some suitable and useful concepts and tools for the understanding and analysis of approximate correctness of programs in concurrent systems. Throughout this book the focus is on the framework of process calculus, and the main idea is to construct some natural and reasonable topological structures which can reveal suitably a mechanism of approximate computation in process calculus and to work out various relationships among processes which are compatible with these topological structures.

Good syntax for single argument methods?

I'm looking for good non-brace syntax for a single argument method call. I can't use space since it is already taken for infix operations (e.g. x + y vs. draw circle(...)). I was thinking about using hash; e.g. draw#circle(....) where circle is a method that produces a circle shape to draw. Are there any better options that have been tried before?

As for why I don't just go with braces, I'm looking for a special syntax to capture "verb on what" in a way that can more easily be read left to right without nesting.

VISSOFT 2015 - Call for Papers: New Ideas or Emerging Results and Tool Demos

VISSOFT 2015 - Call for Papers: New Ideas or Emerging Results and Tool Demos

3rd IEEE Working Conference on Software Visualization (VISSOFT)
September 27-28, 2015, Bremen, Germany

Paper submission date: June 29, 2015
Notification: July 31, 2015

Software visualization is a broad research area encompassing concepts, methods, tools, and techniques that assist in a range of software engineering and software development activities. Covered aspects include the development and evaluation of approaches for visually analyzing software and software systems, including their structure, execution behavior, and evolution.

The VISSOFT IEEE Working Conference on Software Visualization continues the history of the ACM SOFTVIS Symposium on Software Visualization and the IEEE VISSOFT International Workshop on Visualizing Software for Understanding and Analysis. The conference focuses on visualization techniques that target aspects of software maintenance and evolution, program comprehension, reverse engineering, and reengineering, i.e., how visualization helps professionals to understand, analyze, test and evolve software. We aim to gather tool developers, experts, users, and researchers from software engineering, information visualization, computer graphics, and human-computer interaction to discuss theoretical foundations, algorithms, techniques, tools, and applications related to software visualization.

Topics of interest include, but are not limited to:
* Innovative visualization and visual analytics techniques for software engineering data, such as,
- source code
- static and dynamic dependencies
- software evolution and repositories
- software documentation
- web services
- protocol, log, and performance data
- parallel techniques
- database schemes
- software security and privacy issues
- workflow and business processes
* Visualization to support program comprehension, software testing, and debugging
* Interaction techniques and algorithms for software visualization
* Visualization-based techniques in computer science and software engineering education
* Integration of software visualization tools and development environments
* Empirical evaluation of software visualization
* Industrial experience on using software visualization

VISSOFT features a New Ideas or Emerging Results (NIER) track and a Tool Demo track related to the list of topics suggested above. Papers are solicited that present original, unpublished research results and will be rigorously reviewed by an international program committee.

The NIER contributions (New Ideas and Emerging Results) describe work-in-progress and preliminary exciting results. Authors should include open questions and even provocative hypotheses to get early feedback on their research ideas or even support through new research collaborations.

Tool contributions describe the design or actual utilization of software visualization tools, with a focus on relevant tool construction aspects or the use of the tool for gaining new insights. Authors should be prepared to demonstrate their tool at the conference. The submission may also contain a link to a screencast (video).

All accepted submissions will appear in the conference proceedings and the IEEE Digital Library.

-== How to Submit ==-

Both types of papers have to be maximum 5 pages long (including bibliography and annexes).
Paper submission date: June 29, 2015 (previously: June 15, 2015)
Notification: July 31, 2015

Submissions must be submitted online via the VISSOFT 2015 EasyChair
conference management system at

Please adhere to the formatting instruction published on the ICSME

-== Organizing Committee ==-

General Chair:
Jürgen Doellner, Hasso-Plattner-Institut, Germany

Program Co-Chairs:
Fabian Beck, University of Stuttgart, Germany
Alexandre Bergel, University of Chile, Chile

NIER/Tool Co-Chairs:
Craig Anslow, Middlesex University, UK
Johan Fabry, University of Chile, Chile

NIER/Tool Program Committee:

Bilal Alsallakh TU Vienna, Austria
Jennifer Baldwin Swinburne University,Australia
Ivan Beschastnikh University of British Columbia, Canada
Usman Bhatti INRIA Lille / Synectique, France
Michael Burch University of Stuttgart, Germany
Andrei Chis Bern University, Switzerland
Neville Churcher University of Canterbury, New Zealand
Marcus Denker INRIA Lille, France
Coen De Roover Vrije Universiteit Brussel, Belgium
Jens Dietrich Massey University, New Zealand
Bogdan Dit Boise State University, US
Matthias Frisch Magdeburg University, Germany
Maria-Elena Froese University of Victoria, Canada
Michael Homer Victoria University of Wellington, New Zealand
James A. Jones University of California, Irvine, US
Adrian Kuhn AirBNB, US
Jannik Laval Ecole Des Mines de Douai, France
Paul Leger Universidad Catolica Del Norte, Chile
Andrea Mocci University of Lugano, Switzerland
Tim Molderez Vrije Universiteit Brussel, Belgium
Chris Parnin NC State University, US
Michael Perscheid HPI-Universtat Potsdam, Germany
David Roethlisberger Universidad Diego Portales, Chile
Christian Tominski University of Rostock, Germany

Symbol Flux: abstract visual debugging Abstract:

Do you ever wish you could just see some table or tree (or graph, list or hashmap) while programming?

I want to be able to do that all the time, without having to work for it. So, I'm writing an 'abstract visual debugger' to that end, and this is what it looks like so far:


XKCD on type theory...

Just thought people might find this amusing.

The hell of this is I can tell exactly which languages he's making fun of in almost 75% of those lines.

Edit: I would use the "embedding url" with an html tag containing


but LTU refuses to display it.

Functors are Type Refinement Systems

Functors are Type Refinement Systems
Paul-André Melliès and Noam Zeilberger
POPL 2015

The standard reading of type theory through the lens of category theory is based on the idea of viewing a type system as a category of well-typed terms. We propose a basic revision of this reading: rather than interpreting type systems as categories, we describe them as functors from a category of typing derivations to a category of underlying terms. Then, turning this around, we explain how in fact any functor gives rise to a generalized type system, with an abstract notion of typing judgment, typing derivations and typing rules. This leads to a purely categorical reformulation of various natural classes of type systems as natural classes of functors.

The main purpose of this paper is to describe the general framework (which can also be seen as providing a categorical analysis of refinement types), and to present a few applications. As a larger case study, we revisit Reynolds' paper on "The Meaning of Types" (2000), showing how the paper’s main results may be reconstructed along these lines.

This paper was quite a joy to read. The proposed framework feels simple yet penetrating, with convincing examples of elementary categorical constructions translating to non-trivial type system features. According to the second author, it is only the first in a series, with a much more advanced second one already available as a draft on the arXiv; I hope that this develops into a useful foundational setting for programming languages.

Structuring F# Programs with Abstract Data Types [Presentation on Vimeo]

I'm hoping this presentation about structuring functional programs could generate some interesting discussion here :) I gave this talk at the New York City F# meetup not too long ago.

Synopsis: A question many people who are new to functional programming ask is, "what does a functional program look like?" Of course, they're not asking about the appearance of individual functions. Instead they are asking what the structure of a functional program should look like, in the abstract. And further, how to go about building one. This talk presents a powerful, composable, and general means of building well-structured functional programs, specifically in F#. Presented is a singular, simple functional 'design pattern' that can be applied recursively to architect principled F# programs. Like any pattern, it's applicability is not total. However, for those looking start architecting beautiful functional programs, frameworks, and engines in F#, this is a great first approach to consider.

Check it out here.

Slides and examples are also available here.

Fixed points considered harmful

Fixed points have been an important topic ever since Church invented the lambda calculus in the early 1930s.

However, the existence of fixed points has unfortunate consequences:
* In a programming language, they preclude having having strong types
* In logic, they lead to inconsistency.

Fortunately, types intuitively preclude the existence of fixed points, e.g.,
ActorScript and Direct Logic.

Paper journals are in bad shape; priority established in HAL ...

In Computer Science, paper-based journals are in bad shape with unpaid refereeing not adding much value to articles. Papers are debugged by colleagues (including students). Also, page limits are a huge limitation of page-based journals.

Publication in a paper-based journal is often for reasons like the following:
* political, e.g., tenure, public policy, etc.
* publicity and branding, e.g., CACM is often considered "first-rank"

Important information typically travels first electronically with publication in a paper-based journal sometimes following years later, if at all. Priority is often established by publication in HAL, etc. Books, (e.g. "Inconsistency Robustness") can be important in collecting and summarizing.

XML feed