thomasbarker.com I just build stuff

Type-Checking Zero Knowledge

This paper presents the first type system for statically analyzing security protocols that are based on zero-knowledge proofs. We show how certain properties offered by zero-knowledge proofs can be characterized in terms of authorization policies and statically enforced by a type system. The analysis is modular and compositional, and provides security proofs for an unbounded number of protocol executions. We develop a new type-checker that conducts the analysis in a fully automated manner. We exemplify the applicability of our technique to real-world protocols by verifying the authenticity and secrecy properties of the Direct Anonymous Attestation (DAA) protocol. The analysis of DAA takes less than three seconds.

A little dependent type theory, a little Pi calculus, a little cryptography... there's something for everyone! This is follow-up work to this story that Ehud posted.

The source code can be found here.

There's a new entry on Combinatory Logic in the Stanford Encyclopedia of Philosophy.

I haven't perused it yet, so please share opinions and comments.

Surprised to see there hasn't been a mention of Microsoft's recent PDC. They have some interesting talks available on the web.

There are a couple of videos on "Oslo," their DSL framework. Discussion of finding bugs in concurrent programs. An introduction to F#. For me, the most interesting, and the most unexpected talk was on contracts being integrated into .NET as a library. These pre/post conditions and invariants can be checked at compile time and another project "Pex" can use them to generate unit tests.

Modeling Abstract Types in Modules with Open Existential Types, by Benoît Montagu Didier Rémy:

We propose F¥, a calculus of open existential types that is an extension of System F obtained by decomposing the introduction and elimination of existential types into more atomic constructs. Open existential types model modular type abstraction as done in module systems. The static semantics of F¥ adapts standard techniques to deal with linearity of typing contexts, its dynamic semantics is a small-step reduction semantics that performs extrusion of type abstraction as needed during reduction, and the two are related by subject reduction and progress lemmas. Applying the Curry-Howard isomorphism, F¥ can be also read back as a logic with the same expressive power as second-order logic but with more modular ways of assembling partial proofs. We also extend the core calculus to handle the double vision problem as well as type-level and term-level recursion. The resulting language turns out to be a new formalization of (a minor variant of) Dreyer’s internal language for recursive and mixin modules.

This approach to existentials seems to considerably improve their power and simplify their use. It also brings us one step closer to first-class modules!

The process of programming language creation is a subject of too little reflection and retrospection. Newcomers to the field (including, in some measure, us) regularly propose new languages without quite understanding what they are getting into or how big the task is.
... This paper describes the motivation and early design evolution of the BitC programming language, making our excuses in hindsight and providing a compilation of some of the things that we learned along the way.
... The ML module system [18] is fully understood only by David MacQueen, and only on alternating weeks. The Scheme module system [8] required the combined brilliance of Matt Flatt and Matthias Felleisen (and six revisions of the language standard) to achieve. From the perspective of a mere operating systems weenie, it's all rather discouraging, but what is the reluctant programming language designer to do?
... The real reason we stuck with the LISP-ish syntax is that we didn't want to be fiddling with the parser while designing the language, and (to a lesser degree) because we didn't want to encourage programmers until we thought the language was ready.

The Origins of the BitC Programming Language Warning: Work in Progress

As a result of a refereeing request, I took a look at the website of College Publications, and was very pleased with what I saw. It is a non-profit publisher founded by Jane Spurr and the omnipresent (at least in logic) Dov Gabbay. From their "About us" page:

...objectives...:

• To bring College Publications to a level with Oxford (OUP) and Cambridge (CUP) in terms of publishing capability.
• To provide the community with a non-profit making, highly prestigious publishing outlet that will break the monopoly that commercial publishers have.
• To publish books that can be purchased at reasonable prices, making information accessible to all.

Accordingly, College Publications can publish books at a range of 15–25 dollars per average 300 page book, giving substantially better royalties to authors than other publishers.

...

College Publications does not take copyright and authors are free to use their material elsewhere, and even to put the book on the web once sales have achieved profitability.

The existence of this publisher is very good for the kind of things that LtU stands for in much the same way that Logical Methods in Computer Science is, and supposedly community focussed organisations such as the ACM are not. Take a look at their PL offerings in their computing series, edited by Ian Mackie.

The 1972 paper by Alan Kay, in commemoration of the 40th anniversary of the Dynabook. (via Coding Horror.)

This note speculates about the emergence of personal, portable
information manipulators and their effects when used by both
children and adults. Although it should be read as science
fiction, current trends in miniaturization and price reduction
almost guarantee that many of the notions discussed will actually
happen in the near future.

Type Checking with Open Type Functions by Tom Schrijvers, Simon Peyton-Jones, Manuel M. T. Chakravarty, and Martin Sulzmann

We report on an extension of Haskell with open type-level functions and equality constraints that unifies earlier work on GADTs, functional dependencies, and associated types. The contribution of the paper is that we identify and characterise the key technical challenge of entailment checking; and we give a novel, decidable, sound, and complete algorithm to solve it, together with some practically-important variants. Our system is implemented in GHC, and is already in active use.

Related to GHC/Type families, which can be an important optimization technique when specializing the types. Type families allow greater control over types. I guess they didn't like having C++ templates having any advantage with associated types. Personally, it reminds me of some of the power afforded by ML parameterized functors.

(via reddit and 2 Minute intro to Associated Types/Type Families).

Factor: an extensible interactive language, Google Tech Talk by Slava Pestov.

Factor is a general-purpose programming language which has been in development for a little over five years and is influenced by Forth, Lisp, and Smalltalk. Factor takes the best ideas from Forth -- simplicity, succinct code, emphasis on interactive testing, meta-programming -- and brings modern high-level language features such as garbage collection, object orientation, and functional programming familiar to users of languages such as Python and JavaScript. Recognizing that no programming language is an island, Factor is portable, ships with a full-featured standard library, deploys stand-alone binaries, and interoperates with C and Objective-C.

In this talk, I will give the rationale for Factor's creation, present an overview of the language, and show how Factor can be used to solve real-world problems with a minimum of fuss. At the same time, I will emphasize Factor's extensible syntax, meta-programming and reflection capabilities, and show that these features, which are unheard of in the world of mainstream programming languages, make programs easier to write, more robust, and fun.

An introductory overview article about static analysis tools and how they can be used to improve software security. The article talks a bit about the history of Cigital's ITS4 tool.

Chuck Thacker is building a new research computer called the BEE3.

There was a time, years ago, when computer architecture was a most exciting area to explore. Talented, young computer scientists labored on the digital frontier to devise the optimal design, structure, and implementation of computer systems. The crux of that work led directly to the PC revolution from which hundreds of millions benefit today. Computer architecture was sexy.

These days? Not so much. But Chuck Thacker aims to change that.

To understand the importance of such machines in computing history remember what Alan Kay says of the predecessor used to develop Smalltalk at Xerox PARC:

We invented the Alto and it allowed us to do things that weren’t commercially viable until the 80’s. A research computer is two cubic feet of the fastest computing on the planet. You make it, then you figure out what to do with it. How do you program it? That’s your job! Because real thinking takes a long time, you have to give yourself room to do your thinking. One way to buy time is to use systems not available to most people.

I want one!

Lengrand & Miquel (2008). Classical Fω, orthogonality and symmetric candidates. Annals of Pure and Applied Logic 153:3-20.

We present a version of system Fω, called Fω^C, in which the layer of type
constructors is essentially the traditional one of Fω, whereas provability
of types is classical. The proof-term calculus accounting for the classical
reasoning is a variant of Barbanera and Berardi’s symmetric λ-calculus.
We prove that the whole calculus is strongly normalising. For the
layer of type constructors, we use Tait and Girard’s reducibility method
combined with orthogonality techniques. For the (classical) layer of terms,
we use Barbanera and Berardi’s method based on a symmetric notion of
reducibility candidate. We prove that orthogonality does not capture the
fixpoint construction of symmetric candidates.

We establish the consistency of Fω^C, and relate the calculus to the
traditional system Fω, also when the latter is extended with axioms for
classical logic.

We last mentioned this book back in 2005, when the text was available as a series of drafts, and LtU user raould updated the post back in late August letting LtU readers know you can get it from MIT Press, but to be sure: the book is out. Not to play favorites, but Amazon currently has it new for $54 USD, and it retails for $75 USD. Powell's currently has one copy in stock as well (thanks Tim!).

And it's massive. At 1,322 numbered pages, it'll take me a while to get through, but I hope to post a review once I'm done. LtU readers might be interested to know that the book is based on and is now used in MIT's graduate programming languages course, 6.821.

A rather amusing thread on the plt-scheme mailing list, reminded me of Wadler's paper Why Calculating is Better than Scheming from 1987, which wasn't discussed here as far as I recall.

It's a bit of a blast from the past, but still worth reading.

Peteris Krumins has been posting his notes on MIT’s Introduction to Algorithms. The notes are valuable for anyone interested in working their way through the CLRS text and MIT Open Courseware videos.

I just finished watching the last lecture of MIT’s "Introduction to Algorithms" course. Having a great passion for all aspects of computing, I decided to share everything I learned...

Although not directly tied to programming languages, every PL has to eventually be able to express algorithms. Aside from Knuth, CLRS is probably the closest approximation to a comprehensive approach to algortihms. The text itself is language agnostic - the authors use their own brand of pseudo-code to describe the algorithms. This has the advantage of allowing the reader to focus on the algorithms at a higher level, rather than get bogged down in the specifics of any PL. The downside, at least in my estimation, is that the authors don't make it particularly easy to implement the algorithms in any specific PL. The pseudo code conflates common data structures (such as arrays) with properties/attributes that can be tagged with those structures. And some of the algorithms refer to variables that are outside of the scope of the function. Also, like Knuth, most of the algorithms are steeped in state, making it hard to implement them with functional programming approaches.

That said, the video lectures and the accompanying notes above are good resources for any that want to self-study CLRS. Here are the notes thus far:

• Lectures 1 and 2: Analysis of Algorithms
• Lecture 3: Divide and Conquer
• Lectures 4 and 5: Sorting
• Lecture 6: Order Statistics
• Lectures 7 and 8: Hashing
• Lectures 9 and 10: Search Trees
• Lecture 11: Augmenting Data Structures
• Lecture 12: Skip Lists

Via Patrick (who was once a LtU contributor), two interesting blog posts:

• A discussion of the uses of Lua in Lightroom and about the use of dynamic language to develop desktop software in general (blog post by a LtU member). Apparently, some 63% of the code written by the Adobe Lightroom team is in Lua.
• A brief history of IBM's Visual Age, originally written in Smalltalk (the product, not the blog post), and Digitalk (remember Digitalk?!).

Story on Nabble here. Release note highlights:

Objective Caml 3.11.0:
----------------------

(Changes that can break existing programs are marked with a "*" )

Language features:
- Addition of lazy patterns: "lazy " matches suspensions whose values,
after forcing, match the pattern .
- Introduction of private abbreviation types "type t = private ",
for abstracting the actual manifest type in type abbreviations.

Compilers:
* The file name for a compilation unit must correspond to a valid identifier
(no more "test-me.ml" or "my file.ml".)
* Revised -output-obj: the output name must now be provided; its
extension must be one of .o/.obj, .so/.dll, or .c for the
bytecode compiler. The compilers can now produce a shared library
(with all the needed -ccopts/-ccobjs options) directly.
- With -dtypes, record (in .annot files) which function calls
are tail calls.
- All compiler error messages now include a file name and location.
- Optimized compilation of "lazy e" when the argument "e" is
already evaluated.
- Optimized compilation of equality tests with a variant constant constructor.
- The -dllib options recorded in libraries are no longer ignored when
-use_runtime or -use_prims is used (unless -no_auto_link is
explicitly used).
- Check that at most one of -pack, -a, -shared, -c, -output-obj is
given on the command line.
- Optimized compilation of private types as regular manifest types
(e.g. abbreviation to float, float array or record types with only
float fields).

Native-code compiler:
- A new option "-shared" to produce a plugin that can be dynamically
loaded with the native version of Dynlink.
- A new option "-nodynlink" to enable optimizations valid only for code
that is never dynlinked (no-op except for AMD64).
- More aggressive unboxing of floats and boxed integers.
- Can select with assembler and asm options to use at configuration time.

Run-time system:
- Changes in freelist management to reduce fragmentation.
- New implementation of the page table describing the heap (a sparse
hashtable replaces a dense bitvector), fixes issues with address
space randomization on 64-bit OS (PR#4448).
- New "generational" API for registering global memory roots with the GC,
enables faster scanning of global roots.
(The functions are caml_*_generational_global_root in .)
- New function "caml_raise_with_args" to raise an exception with several
arguments from C.
- Changes in implementation of dynamic linking of C code:
under Win32, use Alain Frisch's flexdll implementation of the dlopen
API; under MacOSX, use dlopen API instead of MacOSX bundle API.

Standard library:
- Parsing library: new function "set_trace" to programmatically turn
on or off the printing of a trace during parsing.
- Printexc library: new functions "print_backtrace" and "get_backtrace"
to obtain a stack backtrace of the most recently raised exception.
New function "record_backtrace" to turn the exception backtrace mechanism
on or off from within a program.
- Scanf library: debunking of meta format implementation;
fscanf behaviour revisited: only one input buffer is allocated for any
given input channel;
the %n conversion does not count a lookahead character as read.

Other libraries:
- Dynlink: on some platforms, the Dynlink library is now available in
native code. The boolean Dynlink.is_native allows the program to
know whether it has been compiled in bytecode or in native code.
- Bigarrays: added "unsafe_get" and "unsafe_set"
(non-bound-checking versions of "get" and "set").
- Bigarrays: removed limitation "array dimension - Labltk: added support for TK 8.5.
- Num: added conversions between big_int and int32, nativeint, int64.
More efficient implementation of Num.quo_num and Num.mod_num.
- Threads: improved efficiency of mutex and condition variable operations;
improved interaction with Unix.fork (PR#4577).
- Unix: added getsockopt_error returning type Unix.error.
Added support for TCP_NODELAY and IPV6_ONLY socket options.
- Win32 Unix: "select" now supports all kinds of file descriptors.

Tools:
- ocamldebug now supported under Windows (MSVC and Mingw ports),
but without the replay feature. (Contributed by Sylvain Le Gall
at OCamlCore with support from Lexifi.)
- ocamldoc: new option -no-module-constraint-filter to include functions
hidden by signature constraint in documentation.
- ocamlmklib and ocamldep.opt now available under Windows ports.
- ocamlmklib no longer supports the -implib option.
- ocamlnat: an experimental native toplevel (not built by default).

Bug fixes:
- Major GC and heap compaction: fixed bug involving lazy values and
out-of-heap pointers.
- PR#3915: updated some man pages.
- PR#4261: type-checking of recursive modules
- PR#4308: better stack backtraces for "spontaneous" exceptions such as
Stack_overflow, Out_of_memory, etc.
- PR#4338: Str.global_substitute, Str.global_replace and the Str.*split*
functions are now tail-recursive.
- PR#4503: fixed bug in classify_float on ARM.
- PR#4512: type-checking of recursive modules
- PR#4517: crash in ocamllex-generated lexers.
- PR#4542: problem with return value of Unix.nice.
- PR#4557: type-checking of recursive modules.
- PR#4562: strange %n semantics in scanf.
- PR#4564: add note "stack is not executable" to object files generated by
ocamlopt (Linux/x86, Linux/AMD64).
- PR#4566: bug in Ratio.approx_ratio_fix and Num.approx_num_fix.
- PR#4582: weird behaviour of String.index_from and String.rindex_from.
- PR#4583: stack overflow in "ocamlopt -g" during closure conversion pass.
- PR#4585: ocamldoc and "val virtual" declarations.
- PR#4587: ocamldoc and escaped @ characters.
- PR#4605: Buffer.add_substitute was sometime wrong when target string had backslashes.
- PR#4614: Inconsistent declaration of CamlCBCmd in LabelTk library.

Now for some unfortunate news:

Native dynlink used to work on Mac OS X

The clean solution to make natdynlink work on recent Mac OS X systems (beside convincing Apple to support the old behavior of their linker in their new implementation) is to change OCaml's x86 backend so that it produces only PIC code (this has been done for the AMD64 port). I don't think there is currently any plan to work on that.

...

Ouch, this makes it almost a dead end for us. I can offer some time to help in this effort, working in the port, or providing feedback. The native dynlink and toplevel are, at least to me, the killer features in 3.11, but adding another hole for Mac OS X intel (in addition to not supporting x86_64) does not seem like the best choice for an increasingly popular architecture.

...

Well, we'd very much like to support native dynlink on OS X 10.5, but Apple is not helping in the least by crippling their linker compared with the one in 10.4. If anyone from Apple is on this list, feel free to contact us at caml-devel@... for more information on this regression.

So it seems like OCaml needs help along two dimensions: support for the X86_64 in general, and support for Position-Independent Code (PIC) in particular. At least on the PIC side, we can steal from the AMD64 port.

In very disappointing news proper tail calls are out of ES4. It seems that a justification for tail calls could not be found. For example, here is Adobe's position on tail calls:

A more serious point is that we can't avoid adding tail calls at some point if we cater to the functional programming crowd. However, if we really intend to cater to them then we need to provide data structures that are functional too, like lists and operations on them—unlike ES arrays, which are entirely imperative. Of course users can implement those data structures themselves, if they have tail calls, but right now just adding tail calls “for functional programming” seems like a half solution.

Finally, tail calls preclude the use of straightforward implementation techniques for procedure calls. To be sure they are less limiting than generators, as one-shot continuations or longjumps are sufficient to handle tail calls in a non-tail-calling implementation language, but implementations that want good-performance tail calls must necessarily switch to a code generation technique.

This seems misguided. The user can implement functional data structures but not tail calls (without whole program transformation), so the later are much more valuable than the former. Furthermore, as a functional programmer I'm quite happy to use mutable data structures but I would certainly miss tail calls. Finally, every JS implementation is already shifting to code generation because straightforward implementation techniques are too slow for the existing idioms used in JS code.

The ES4 Wiki still indicates that tail calls are in, so perhaps they'll yet make it. For laughs you might want to look at the Ecmascript progress spreadsheet. Apple sure don't like change.

A nice viedo interview of Anders Hejlsberg and Guy Steele on Concurrency and Language Design at the JAOO conference. Nothing too technically deep, but the interview does manage to crystalize some of the high level issues that face language designers.

Speaking of interviews, the Lisp50 Conference at OOPLSA 2008 will have what should prove interesting - Alan Kay interviewing John McCarthy.

Worlds: Controlling the Scope of Side Effects by Alessandro Warth and Alan Kay, 2008.

The state of an imperative program -— e.g., the values stored in global and local variables, objects’ instance variables, and arrays—changes as its statements are executed. These changes, or side effects, are visible globally: when one part of the program modifies an object, every other part that holds a reference to the same object (either directly or indirectly) is also affected. This paper introduces worlds, a language construct that reifies the notion of program state, and enables programmers to control the scope of side effects. We investigate this idea as an extension of JavaScript, and provide examples that illustrate some of the interesting idioms that it makes possible.

This introduces a new programming construct that's just the kind I love: they stimulate the imagination and provide simple and strong dynamic invariants to make programs easy to reason about.