The Automath Archive was created by the Brouwer Institute in Nijmegen and the Formal Methods section of Eindhoven University of Technology. Started by prof. H. Barendregt, in cooperation with Rob Nederpelt, this archive project was launched to digitize valuable historical articles and other documentation concerning the Automath project.

Initiated by prof. N.G. de Bruijn, the project Automath (1967 until the early 80's) aimed at designing a language for expressing complete mathematical theories in such a way that a computer can verify the correctness. This project can be seen as the predecessor of type theoretical proof assistants such as the well known Nuprl and Coq.
(Introduction copied from the website, hope that is allowed).

Ehud, I hope this satisfies your wish for historical CS subjects.

Alan Turing

The Turing Archive for the History of Computing is a major Internet project. The site is currently scheduled for completion by the end of 2004. We hope you will enjoy—and learn from—what we have done so far.

The documents that form the historical record of the development of computing are scattered throughout various archives, libraries and museums around the world. Until now, to study these documents required a knowledge of where to look, and a fistful of air tickets. This Virtual Archive contains digital facsimiles of the documents. The Archive places the history of computing, as told by the original documents, onto your own computer screen.

This site also contains a section on codebreaking and a series of reference articles concerning Turing and his work.

(Introduction copied from the website, hope that is allowed)

Found this site while wandering about on the internet. Didn't see any reference to it on Ltu.

Proofs are Programs: 19th Century Logic and 21st Century Computing

Proofs are Programs: 19th Century Logic and 21st Century Computing

As the 19th century drew to a close, logicians formalized an ideal notion of proof. They were driven by nothing other than an abiding interest in truth, and their proofs were as ethereal as the mind of God. Yet within decades these mathematical abstractions were realized by the hand of man, in the digital stored-program computer. How it came to be recognized that proofs and programs are the same thing is a story that spans a century, a chase with as many twists and turns as a thriller. At the end of the story is a new principle for designing programming languages that will guide computers into the 21st century.

This paper by Philip Wadler was a Dr Dobbs article in 2000 and has a matching a Netcast interview.

This nifty paper starts with Frege's Begriffschrift in 1879 and goes to Gentzen's sequent calculus, Church's untyped and then typed lambda calculus, and then brings it all together to describe the Curry-Howard correspondence. For the grand finale, Wadler connects this to Theorem Provers and Proof Carrying Code and gives commercial examples where it all pays off.
This is an enjoyable story and a fun introduction to type theory and the Curry-Howard correspondence.

For more of Wadler's writings along these lines check out his History of Logic and Programming Languages paper collection.

edit: fixed the dr dobbs article link

Functional Programming Has Reached The Masses; It's Called Visual Basic

In May I will be speaking at Expo-C in the beautiful town of Karlskrona, an official UN World Heritage Site. It is great to see that all the buzz around LINQ is putting functional programming back in the picture and the organizers have asked me to combine a Haskell tutorial with an overview of LINQ, including C# 3.0 and Visual Basic 9.(*) in addition to my "coming out" talk VB IsNot C#.

This, and the ICFP deadline last Friday have prompted me to write a short memoir of my journey to democratize distributed data-intensive dynamic applications by leveraging the great ides from functional programming. Comments, supplementary information, missing related work, and flames are all most welcome. In particular I am interested to learn if anyone is using H/Direct to use Haskell for programming against XPCOM.

Hope to see you in Sweden, or at any of my other gigs.

(*) I will be using Graham Hutton's excellent slides.

Fortran articles online

I have the pleasure of thanking ACM for granting permission to post the full texts of five ACM-copyrighted articles to the FORTRAN/FORTRAN II web site at the Computer History Museum. Here they are; for those already in the ACM Digital Library, we also link to the canonical ACM version via its DOI (Digital Object Identifier).

Once again we owe a big thank you to Paul McJones.

Guy Steele on Language Design

(via PLNews)
Thoughts on Language Design

Computers with multiple processors are becoming more and more common. We need programming languages that support the use of multiple threads of control. [...] In such a context, the organizing principles of structured programming may not always be appropriate. I'm not talking about avoiding goto. (Java has no goto statement.) I'm talking about sequencing, if-then-else, and loops.

FORTRAN 25th anniversary film online

FORTRAN 25th anniversary film, 1982, 12.5 minutes. Computer History Museum lot number X2843.2005, donated by Daniel N. Leeson. Windows Media Video (12.8 megabytes)

Another great resource from Paul McJones.

The video quality isn't great, but this is still very much worth your time. It's interesting to see the faces behind the history of our discipline.

I am not going to list all the ideas from the film that are worth discussing. Let me just note that several remarks at the begining show just how remarkable the notion of a programming language really is (or was, at the time).

The guys discussing Fortress will also find several of the comments made in the film interesting.

MIT CADR Source Snapshot Released

Via Lemonodor. More details can be found at Bill Clementson's Blog.

Link to files

Guido van Rossum: Building an Open Source Project and Community

A long (close to two hours) audio presentation about Python's history and philosophy.

LtU readers will find a lot to disagree with (especially in part 2), for instance when Guido discusses dynamic languages and typing. And yet, I think Guido tries to be reasonable, even though I disagree with some of his conclusions.

Be that as it may, this talk provides a useful summary of Python's history, and some idea about the workings of the Python community. Long time readers will remember that I think language communities play an important, yet under appreciated, role in language evolution and success.

The birth of the FORTRAN II subroutine

By comparing three versions of the memo (unsigned, but believed written by Irv Ziller) “Proposed Specifications for FORTRAN II for the 704″, dated August 28, September 25, and November 18, 1957, you can watch the design of the subroutine feature of FORTRAN II unfold.

Also: separate compilation.

XML feed