Lambda the Ultimate

50 papers...some of them are even related to objects (author/institution names elided for brevity):

1. Input-Covering Schedules for Multithreaded Programs
2. Data-Driven Equivalence Checking
3. Efficient Context Sensitivity for Dynamic Analyses via Calling Context Uptrees and Customized Memory Management
4. Inductive Invariant Generation via Abductive Inference
5. Resurrector: A Tunable Object Lifetime Profiling Technique for Optimizing Real-World Programs
6. Code Optimizations Using Formally Verified Properties
7. CDSChecker: Checking Concurrent Data Structures Written with C/C++ Atomics
8. Empirical Analysis of Programming Language Adoption
9. River Trail: A Path to Parallelism in JavaScript
10. Barrier Invariants: A Shared State Abstraction for the Analysis of Data-Dependent GPU Kernels
11. Online-Feedback-Directed Optimizations for Parallel Java Code
12. Octet: Capturing and Controlling Cross-Thread Dependences Efficiently
13. Semi-Automatic Rename Refactoring for JavaScript
14. Ball-Larus Path Profiling Across Multiple Loop Iterations
15. Combining Concern Input with Program Analysis for Bloat Detection
16. Detecting API Documentation Errors
17. Set-Based Pre-Processing for Points-To Analysis
18. Multiverse: Efficiently supporting distributed high-level speculation
19. On-the-fly Detection of Instability Problems in Floating-Point Program Execution
20. Taking Off the Gloves with Reference Counting Immix
21. Do Developers Benefit from Generic Types? An Empirical Comparison of Generic and Raw Types in Java
22. Bottle Graphs: Visualizing Scalability Bottlenecks in Multi-Threaded Applications
23. Class Hierarchy Complementation: Soundly Completing a Partial Type Graph
24. Storage Strategies for Collections in Dynamically Typed Languages
25. Relaxed Separation Logic: A Program Logic for C11 Concurrency
26. Turning Nondeterminism into Parallelism
27. Isolation for Nested Task-Parallelism
28. Forsaking Inheritance: Supercharged Delegation in DelphJ
29. Python: The Full Monty; A Tested Semantics for the Python Programming Language
30. Miniboxing: Improving the Speed to Code Size Tradeoff in Parametric Polymorphism Translations
31. Effective Race Detection for Event-Driven Programs
32. Efficient Concurrency-Bug Detection Across Inputs
33. On-the-fly Capacity Planning
34. The Latency, Accuracy, and Battery (LAB) Abstraction: Programmer Productivity and Energy Efficiency for Continuous Mobile Context Sensing
35. Flexible Access Control Policies with Delimited Histories and Revocation
36. Interacting with Dead Objects
37. Refactoring with Synthesis
38. Language Support for Dynamic, Hierarchical Data Partitioning
39. Verifying Quantitative Reliability of Programs That Execute on Unreliable Hardware
40. Object-Oriented Pickler Combinators and an Extensible Generation Framework
41. Option Contracts
42. Targeted and Depth-first Exploration for Systematic Testing of Android Apps
43. Ironclad C++: A Library-Augmented Type-Safe Subset of C++
44. Injecting Mechanical Faults to Localize Developer Faults for Evolving Software
45. Guided GUI Testing of Android Applications with Minimal Restart and Approximate Learning
46. Steering Symbolic Execution to Less Traveled Paths
47. MrCrypt: Static Analysis for Secure Cloud Computations
48. Synthesis Modulo Recursive Functions
49. Bounded Partial-Order Reduction
50. Fully Concurrent Garbage Collection of Actors in Many-Core Machines

Formalisation of the λ_א Runtime

This is the formal details paper. The summary/rational paper is apparently due to be published by the ACM next month.

Essay by J. Aldrich to appear at onward! Abstract:

Three years ago in this venue, Cook argued that the essence of objects is procedural data abstraction. His observation raises a natural question: if procedural data abstraction is the essence of objects, has it contributed to the empirical success of objects, and if so, how?

This essay attempts to answer that question. It begins by reviewing Cook’s definition and then, following Kay, broadens the scope of inquiry to consider objects that abstract not just data, but higher-level goals. Using examples taken from object-oriented frameworks, I illustrate the unique design leverage that objects provide: the ability to define abstractions that can be extended, and whose extensions are interoperable. The essay argues that the form of interoperable extension supported by objects is essential to modern software: many modern frameworks and ecosystems could not have been built without objects or their equivalent. In this sense, the success of objects was not a coincidence: it was inevitable.

Programs using Assertions, Goals, and Plans have been proposed as important to the future of program languages ever since Terry Winograd demonstrated SHRDLU using Planner in 1968.

Recently, Robert Kowalski proposed considering a situation posed by the following notice in the London Underground:

                          Emergencies
Press the alarm signal to alert the driver.
The driver will stop if any part of the train is in the station.
If not, the train will continue to the next station, where help can more easily be given.
There is a 50 pound penalty for improper use.

Some of the procedural information for the above is embedded the following using a dialect of modern Logic Programs:

When Assertion Pressed[alarmSignalButton]→ Assert Alerted[driver]▮
When Assertion Alerted[driver]→
   When Assertion InStation[train]→ Assert Stopped[driver, train],
   When Assertion ¬InStation[train]→ Assert ContinuingToNextStation[driver, train]▮
When Assertion ImproperlyUsed[person, alarmSignalButton]→ Assert PenaltyOwed[person, 50 pounds]▮  

Of course, the above program needs to be fleshed out with considerably more code.

How important are Logic Program languages using assertions, goals, and plans to the future?

Bret Victor's The Future of Programming looks at the promising future of programming as it presented itself in 1973 and what we should expect it to be 40 years later, i.e., today. A lot of things that seemed crazy (GUI, Prolog, Smalltak, the Internet) became reality but we might be still held back today by the same skepticism over what constitutes programming as in 1973. At the same time, engineering seems to have carried us a lot farther than Bret Victor is willing to admit. Victor advocates four changes to move programming into the future:

1. from coding to direct manipulation of data
2. from procedures to goals and constraints
3. from programs as text dump to spatial representations
4. from sequential to parallel programs

If nothing else, this an entertaining and well-produced video of his presentation.

I'm designing/implementing a new semi-imperative programming model called Glitch that is based on optimistic execution and eventual consistency. The idea is that a computation can only performs imperative effects that are undoable and commutative so that (1) they can be rolled back when re-execution deems that they are no longer performed and (2) that an effect can be installed in any order so the computation can be decomposed into parts that can be executed in arbitrary order. Few effects are actually commutative, but we can hack some to act commutatively with extra restrictions or data; examples:

• Adding to a set is naturally commutative.
• Aggregation sub-operations (increment, max) are naturally commutative (though max is not easily undoable...).
• Setting a cell element or map entry are not commutative. However, if we enforce "set once" restrictions dynamically, then they appear commutative with the caveat that a second conflicting effect can fail. We must then associate effects with stable execution addresses to determine which effects are conflicting, and which effects have simply changed in what they do.
• Appending a list (or an output log) is not commutative. However, if we order execution addresses, then we can translate append into commutative insertion into a set whose elements are automatically sorted by effect address.

I was wondering if anyone has used commutative effects before? The closest I have found on this topic concerns "commutative monads" where effect ordering doesn't matter. However, they don't seem to be doing many interesting things with them beyond relaxing ordering constraints for parallel computations, and they also don't seem to talk about many interesting commutative effects (just Maybe and Reader?). Also, I wonder how users would feel if they were given a language that restricted some to just imperative effects...would it be overly restrictive or a nice addition to an otherwise pure-ish language?

I'm still writing this up, but the system has been expressive enough for my live programming work (e.g. it can be used to write a compiler).

As we have another thread on avoiding the practical consequences of Godel incompleteness theorem, which seems like a worthwhile goal, I thought I'd post this fun little construction.

To what extent can we implement a provably correct compiler for our language? If we start with axioms of the machine (physical or virtual), can we prove that a compiler correctly implements itself on this target machine? There's a simple construction that works for all sorts of systems that effectively allows you to prove self-consistency without running afoul of Godel's theorem. Here's the idea:

Let's start with your favorite system (set theory, type theory) to which we want to add self-evaluation (to, among other things, prove self-consistency). As a first step, let's add a big set/type on top that's large enough to model that system. For example, in ZFC set theory, you can add an inaccessible cardinal. You're just looking at the original system from the outside and saying "ok, take all of the stuff in that system, and add the ability to quantify over that, getting a new system."

Now this new system that you end up with can model and prove the consistency of the original system, but still cannot prove the consistency of itself. This leads to a simple "practical self-compilation": perform this jump to bigger and bigger systems 2^64 times and start with a version of the compiler at level N=2^64. Whenever you want to do a new compiler, you prove the consistency of the axioms at level N-1. Each version of the compiler has N as part of its axioms and can prove the consistency of "itself" (but for versions with smaller N). No compiler ever proves its own consistency, but, as a practical matter, if the only thing you use these levels compile new versions of the compiler, then you won't ever run out of levels.

But there is an inelegance in having to keep track of levels in such a scheme. The number of levels itself clearly isn't important, and even if it's only a version number that's changing, we clearly haven't really created a "self" compiler. Do we really need that number? What's important is just that the scheme prevents infinite descent of the levels. So here's the proposed fix:

Step 1. Start with some finite number N (leave this N a parameter of the construction; later we'll notice that we can pretend it's infinity) of these inaccessible sets/nested universes and index them so that the biggest one is index 0, the next smallest contained inside it is index 1, etc. Index N is the smallest universe that's just big enough to serve as a model for the original theory.

Step 2. We write a semantic eval function that maps terms in the language into our biggest universe and use it to establish the soundness of the logic/type system. Terms reference 'universe 0' gets mapped to universe 1, 'universe 1' gets mapped to universe 2, etc. Our model of the term for 'N' is N-1 in the model. This step works just like the "first practical solution" above, except now we're counting down and we don't use actual numbers for N in our logic.

Step 3. How do we establish that the new 'N' (N-1) is positive? We make our compiler superstitious as follows: we pick an unused no-op of the target machine that should never occur in normal generated code and add an axiom that says that running this no-op actually bumps a counter that exists in the ether, and, if this unseen counter exceeds N, then it halts execution of the machine. Since we could have started with an arbitrary N, we will never reach a contradiction if we take the bottom out of the level descent, so long as we don't let the logic know we took the bottom out.

Then we can have an inference rule in the logic that allows us to conclude that N > M for any particular M:Nat, without any way to infer that (forall M:Nat. N > M), which would lead to contradiction. The implementation of this inference rule invokes the magic no-op until it's confident that enough such levels exist. Rather than a direct statement that the compiler works, we will have a clause that says "if there are enough levels, then the compiler terminates and works." Any human reading this clause can safely this clause (we know there are always sufficiently many levels), and just as importantly, we can instruct the compiler to allow execution of functions that terminate if there are enough levels and that will make things total. i.e. We can have a total self-compiler.

I have a logic that I'm working with that I'd like to try building this scheme with, but I have quite a bit of work left on the machinery I'd need to complete it. Please let me know if you know of someone who does something similar.

Apologies for the long post. I've argued here that this is possible, but with fewer details. Let me know if I need more details. Hopefully someone finds this interesting.

The issue of consistency has come up in many LtU posts.

Some readers might be interested in the following abstract from Mathematics self-proves its own Consistency:

                   Mathematics self-proves its own Consistency
                          (contra Gödel et. al.)

                             Carl Hewitt
                         http://carlhewitt.info

That mathematics is thought to be consistent justifies the use of Proof by Contradiction.
In addition, Proof by Contradiction can be used to infer the consistency of mathematics 
by the following simple proof:
   The self-proof is a proof by contradiction.
     Suppose to obtain a contradiction, that mathematics is inconsistent.
     Then there is some proposition Ψ such that ⊢Ψ and ⊢¬Ψ¦.
     Consequently, both Ψ and ¬Ψ are theorems
     that can be used in the proof to produce an immediate contradiction.
     Therefore mathematics is consistent.
The above theorem means that the assumption of consistency
is deeply embedded in the structure of classical mathematics.

The above proof of consistency is carried out in Direct Logic [Hewitt 2010]
(a powerful inference system in which theories can reason about their own inferences).
Having a powerful system like Direct Logic is important in computer science
because computers must be able to carry out all inferences
(including inferences about their own inference processes)
without requiring recourse to human intervention.

Self-proving consistency raises that possibility that mathematics could be inconsistent
because of contradiction with the result of Gödel  et. al. that
if mathematics is consistent, then it cannot infer its own consistency. 
The resolution is not to allow self-referential propositions
that are used in the proof by Gödel  et. al.
that mathematics cannot self-prove its own consistency.
This restriction can be achieved by using type theory
in the rules for propositions
so that self-referential propositions cannot be constructed
because fixed points do not exist. 
Fortunately, self-referential propositions
do not seem to have any important practical applications.
(There is a very weak theory called Provability Logic
that has been used for self-referential propositions coded as integers,
but it is not strong enough for the purposes of computer science.) 
It is important to note that disallowing self-referential propositions
does not place restrictions on recursion in computation,
e.g., the Actor Model, untyped lambda calculus, etc.

The self-proof of consistency in this paper
does not intuitively increase our confidence in the consistency of mathematics.
In order to have an intuitively satisfactory proof of consistency,
it may be necessary to use Inconsistency Robust Logic
(which rules out the use of proof by contradiction, excluded middle, etc.).
Existing proofs of consistency of substantial fragments of mathematics
(e.g. [Gentzen 1936], etc.) are not Inconsistency Robust.

A mathematical theory is an extension of mathematics
whose proofs are computationally enumerable.
For example, group theory is obtained
by adding the axioms of groups to Direct Logic.
If a mathematical theory T is consistent,
then it is inferentially undecidable,
i.e. there is a proposition Ψ such that
¬⊢TΨ and ¬⊢T¬Ψ,
(which is sometimes called incompleteness)
because provability in T
is computationally undecidable [Church 1936, Turing 1936].

Information Invariance is a
fundamental technical goal of logic consisting of the following:
  1. Soundness of inference: information is not increased by inference
  2. Completeness of inference: all information that necessarily holds can be inferred
Direct Logic aims to achieve information invariance
even when information is inconsistent
using inconsistency robust inference.
But that mathematics is inferentially undecidable (incomplete)
with respect to ¬ above
does not mean incompleteness
with respect to the information that can be inferred
because it is provable in mathematics that ¬⊢TΨ and ¬⊢T¬Ψ.

The full paper is published at the following location:
Mathematics self-proves its own Consistency

I first wrote to Sean McDirmid about this regarding the previous "Subtyping is a pig" thread here on LtU, and he advised me to post to the forum seeing if anyone's interested and able to engage the material.

I'm going to try to convey here the shortest outline I can manage of the paper I've been brewing. It has been brewing for a number of years, because I do not have any fellow type-theorist to turn to and I'm godawful at writing scientific papers.

Anyway...

Start with a structural type system that has prenex polymorphism and structural subtyping. To integrate for those two, we allow for bounded quantification. How can we go about inferring types for this system in a sound and complete way? Previous proposals (correctly, I think) have pointed to having sets of inequality constraints.

How do I think I'm solving those?

1. I temporarily alter one of the subtyping rules (regarding variable <: variable constraints when both variables are bounded) to read slightly differently, using the Transitive Property of Subtyping.

2. I run an inference procedure in that "modified universe" that is quite similar to unification (takes advantage of structural subtyping rather than nominal). For each type variable \alpha, this procedure finds the smallest convex sublattice (of the total subtyping lattice induced by structural subtyping) containing the concrete types and other free variables constrained to subtype \alpha.

3. I "modify" (invoking Curry-Howard to get my logical soundness here) the inference procedure's results to obtain equivalent typings for the "original universe" with the correct variable <: variable subtyping rule. Specifically, when variables map to a convex sublattice bounded on one end by \top or \bot, I throw out those sublattices and replace those variables with the non-truistic bounds (because \bot <: \alpha means \bot \arrow \alpha, which is a truism).

4. I perform a last step of inference to actually enforce the correct, original variable <: variable subtyping rule where it remains applicable.

At this point, I believe I now have a substitution mapping every type variable to either a concrete type, or a minimal convex sublattice "centered on" that variable.

Anyone interested in this? What have previous approaches to this problem done (I may have heard of them already)? Have other problems ever yielded to an approach like this one?

I can zoom in on any part of the logic if necessary.

Thanks and cheers,
Eli

Hi all,

I'm pleased to announce the 0.6.0 release of Pythonect: http://www.pythonect.org

Pythonect is a new, experimental, general-purpose dataflow programming language based on Python. It provides both a visual programming language and a text-based scripting language. The text-based scripting language aims to combine the quick and intuitive feel of shell scripting, with the power of Python. The visual programming language is based on the idea of a diagram with “boxes and arrows”.

Pythonect interpreter (and reference implementation) is a free and open source software written completely in Python. It is available under the the BSD 3-Clause License.

Highlights for this release include:

* Support for parsing and running Microsoft Visio 2007 and 2010 VDX's (Visio XML Diagrams)

* Support for parsing and running Dia (both compressed, and not compressed diagrams)

* Any Python function can be a reduce()-like using the `_!` identifier (e.g. [1,2,3] -> sum(_!) -> print will print 6)

For more details about the new release please visit:
    http://docs.pythonect.org/en/latest/changelog.html#what-s-new-in-pythonect-0-6

Download page: https://pypi.python.org/pypi/pythonect

* Homepage: http://www.pythonect.org
* Documentation: http://docs.pythonect.org
* GitHub repository: http://github.com/ikotler/pythonect

Please try out this new release and let me know if you experience any problem by filing issues on the bug tracker.

Thanks in advance.