Optimus Prime

I am a Ph.D student within the Programming Languages and Systems (PLASMA) research group. My Ph.D, co-supervised by Professors Colin Runciman and Richard Paige, is investigating the formal verification of functional language implementations. My interests generally lie within the topics of functional languages (in particular, Haskell), semantics and formal methods.

Application have closed for the PLASMA summer internship.

We may have to interview and will inform candidate accordingly. We will be making a decision over the next week.

Summer Internship with PLASMA

Apparently LSCITS has money set aside to fund a few summer internships mentored by the postgraduate researchers. As a man of many ideas but little time, seems like a good opportunity to get some things implemented.

I have one concrete proposal, outlined below. Feel free to suggest your own ideas too, as long as they’re within my field of interest.

Interns will be paid at a rate of £250 per week. You will likely be invited to present your results at the next LSCITS Symposium, to be held in London during the first week of November.

An F-lite to MicroBlaze compiler

When discussing the Reduceron’s performance, we tend to compare it to the execution of the equivalent program compiled in GHC on an x86 architecture. This isn’t entirely fair given that x86 exists in fixed silicon and clocks several times higher than the Reduceron’s FPGA implementation.

A better comparison may be to something like the MicroBlaze Soft Processor, a traditional processor architecture implemented on a Xilinx FPGA. In order to make this comparison, a compiler from F-lite to MicroBlaze instructions is required.

There are a number of possible approaches;

  • Using the LLVM intermediate language and tool chain. It can target MicroBlaze baremetal and has been used very effectively in the latest versions of GHC.
  • Find ways to execute GHC compiled code, baremetal, on MicroBlaze.
  • Update and optimise the F-lite to C compiler.
  • Using similar functional language to C compiler.

Time estimate: 7 – 8 weeks. Recommend familiarity or even just a passing interest in functional programming, functional language implementations and/or low-level programming. Experience with MicroBlaze architecture is a bonus.

Application

If you are interested and are planning to spend the summer in York, please e-mail me at firstname@cs.york.ac.uk by the Tuesday Week 6, 31st May.

I would like to know;

  • Your thoughts on the project and how you would approach it.
  • What related experience you have either academically (CGO, FUN, EDI, EMS, e.t.c.) or in other work.
  • What dates you plan to be available to work.

Depending on a multitude of variables, I may arrange for you to come in and have a further chat.

Eligibility

Applicants must;

  • be a “middle years” student. i.e. 2nd to 3rd year or 3rd to 4th year.
  • satisfy the EPSRC’s residency rules.

More information on eligibility can be found at;

Other LSCITS interships

I’m not the only one offering an LSCITS internship.

Google Code Jam 2011

I didn’t quite get my efficient solution for qualification problem C done in time for the competition.

I might start earlier next time.

Building Agda inside a Capri sandbox

I regularly hit Cabal dependency hell. Every few months (sometimes weeks) I’ve got to throw away my Cabal packages and start again. Well no more! I hope that by sandboxing some of the more agitated packages, maybe I won’t hit that same problem. As a first year student said to me, you “put the rabbits in cages for spring approach.”

Everything went to pot when I tried to install a dev version of Agda today, so it seemed like it was a sensible time to try the theory. I’m using the capri tool to handle the sandboxing. I tried cabal-dev too but capri seemed to help me find the solution more easily.

Please note that the attached script isn’t so much a script. More of a guide.

More heresy

In case anyone was wondering, this rampage was born out of a stackoverflow question.

My answer at the time was "no, because..." but I feel now I can confidently say "you wouldn't want to but there are some ways you can cheat the effect."

But seriously kids, don't do this at home. Use Agda.

Proofs in Haskell + exts + She

Was waiting for the girlfriend's family to arrive today and thought it might be Fun (capital F) to have a play with She (Strathclyde Haskell Enhancement). Now I know it isn't proper DTP and Agda/Coq/Epigram/e.t.c. have all kinds of constraints that GHC Haskell doesn't to keep proofs sound. But hey, what's a little heresy between friends?

There were two main points where She didn't behave as I would have liked it to, both marked in comments (lines 34 and 56). I'm wondering whether these are my own misunderstandings of the syntax. I also wondered whether it could make a stab at translating the value-level function to their type-level equivalents, given the syntactic translation. At what point couldn't it handle the transformation, I wonder.

The points for unsound proofs, that I could spot, were non-total value-level and type-level functions. Are there other constraints that are being missed off? Are there extra tricks I could use to reduce the risks?

Probably should get back to my Agda proofs.

Update 1: Occurred to me that rather than having seperate classes for each theorem, they're both theorems about a {List}. Code has been updated to reflect this.

Update 2: Conor gave tips which have been added at the bottom.

Update to Problem 3

Edit: Yes I know these are full of grammar and spelling errors. The comments are a bit rushed out.

I've made it so it actually follows the specification now. Seems to have gotten a little verbose. 

Click here to download:
Search.pdf (252 KB)
(download)

Updated code is at http://www-users.cs.york.ac.uk/~jason/Search.lagda

Problem Number 3

Update: Find a better version of this at http://optimusprime.posterous.com/update-to-problem-3

Whilst waiting for my washing to finish, I completed another problem. This one was considerably easier but I'm still not sure if my specification matched the judges internet. Any improvements?

Click here to download:
Search.pdf (203 KB)
(download)

VSTTE competition problem 1 completed in Agda.

I went to VSTTE last week where they posed a number of problems for participants to complete. If I hadn't broken my laptop on the first day, I may well have actually competed but c'est la vie. Anyway, it they seemed like a good set of problems to teach me some verification tools so I have just completed the first exercise in Agda. It seems a little verbose so I hope somebody can simplify it a bit.

Click here to download:
SumMax.pdf (273 KB)
(download)

The code file can be found at http://www-users.cs.york.ac.uk/~jason/SumMax.lagda .

Google sync issue for iPhone sends you to web dead end

UPDATE: It's a frickin' documentation error. Google changed the URL but didn't document it. Here's the proper URL for adding calendars to sync with iPhone: https://www.google.com/calendar/iphoneselect
This still doesn't eliminate the loop I documented, but maybe their intern in charge of this will stop playing Pac-Man one day and fix it.

I had issues when I moved to iOS 4.0 and switched to using the built-in Google connectors. To select the calendars for my google apps domain, I had to surf to
> https://www.google.com/calendar/hosted//iphoneselect
on my iPhone. Replace with your hosted address.