Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Matthias Blume
マティアス ブルーメ
Matthias Blume
Toyota Technological Institute at
Chicago
Current events
The 12th
ACM SIGPLAN International Conference on Functional Programming (ICFP
2007)
Contact and Coordinates
The institute is currently located inside the UofC Press building.
My coordinates there are as follows:
- Matthias Blume, Toyota Technological Institute at Chicago, 1427
East 60th Street, Chicago, IL 60637
- blume (at) tti-c . org
- (773) 834-7494 (voice)
- (773) 834-9881 (fax)
- Google Maps/Earth: 41°47'8.62"N 87°35'24.99"W
- Skype (intermittent)
About me
I am an assistant professor at TTI-C.
Before I joined TTI-C, I spent two years as Member of Technical
Staff in the Computing Sciences
Research department at Bell Labs
in Murray Hill, New Jersey. Prior to that I lived for two years in
Kyoto
where I spent my time at
KURIMS
as a
外国人特別研究員
(aka. "Special Foreign Researcher", more precisely:
a JSPS fellow).
I am interested in design, implementation, and applications of
high-level programming languages. Past and current projects include:
-
The Standard ML of New Jersey (SML/NJ)
compiler. These days I am de facto in charge
of putting out new "working" versions.
- The Compilation
Manager (CM) for SML/NJ. Over time this has
developed into an integral component of SML/NJ.
- NLFFI, a new
foreign-function interface for SML/NJ. Let ML code
manipulate C datastructures directly via an embedding of the C type
system into ML types.
- MLPolyR,
a tiny ML-like
language with row polymorphism, polymorphic record selection and
polymorphic sums, functional record update
and extensible first-class
cases, mutable record fields, and a Hindley-Milner-style
type system with principal types.We are working on a
prototype that currently compiles to native PowerPC code (under Mac
OS X). The language descripetion linked above is seriously
out-of-date at the moment.
- A Semantics for Self-Adjusting Computation
with Umut Acar
and Jake Donham. We
developed the first formalized semantics of the combination of
memoization and change-propagation within the same framework and
prove this semantics consistent and correct (with
respect to a purely functional semantics). We formalized and
machine-checked our proof
using Twelf.
- Semantics of Contracts.
With David McAllester I
developed a set-theoretic
model for Findler and Felleisen's Contracts for Higher-Order
Functions for which the contract-checking algorithm is sound
(i.e., never assigns false blame). More recently we extended this
model to also handle recursive
contracts.
With Robby
Findler I also worked on a reconciliation of the apparent
conflict between the above model and a view
of contracts
as projections by showing that contracts should be viewed
as pairs
of projections.
- Complete Type Inference for ML
with Derek Dreyer.
Damas-Milner-style type inference for Standard ML is incomplete
(which might surprise a few people). We are working on a revised
declarative semantics and a corresponding inference algorithm designed to
close the existing gap.
- Programming language support
for self-adjusting
computation (with
Umut Acar).
- Large-scale modular programming
(with Dave
MacQueen). In a nutshell: Extend the notion of
parameterized modules ("functors") to the case of
libraries.
- TupleScheme, the design of a Scheme-like language with
first-class tuples and procedures that are strictly
single-argument/single-result which, nevertheless, is conservative
in the sense that all currently correct whole Scheme programs
continue to work unchanged.This is still
"vaporware", i.e., I know how to do it, but I have not done it
yet.
- I am interested
in helping to evolve the
design of the language that is currently known
as Standard
ML into a possible successor.
- Nova, a language for
programming network processors. Optimal register
allocation (for some suitable notion of "optimal") via integer
linear programming.
- VSCM, a
light-weight implementation
of Scheme. A
complete implementation of R4RS Scheme plus some extensions (e.g., a
module system) consisting of a portable bytecode interpreter and a
bytecode compiler. The project has been handed over to David
Rush.
Here is the draft of a proposal
for portable SML libraries.
Recent professional activities
Students:
Ph.D. students:
Service on thesis committees:
Teaching
GnuPG key
Last modified: May 29th, 2005