It's been a while since my last update. Anyway, last year, I participated in the seminar Dependently typed programming given by Andres Löh and Doaitse Swierstra. I gave a presentation, or more of a lecture really, about Martin-Löf type theory, the Curry-Howard correspondence and some of its connections with Agda.
Since I thought it would still be useful to share, here are the slides:
Type Systems
Download the slides here.
Sunday, 1 May 2011
Monday, 28 June 2010
Linking Interaction Nets and Post Canonical Systems
And one more update due to a paper I wrote for the Models of Computation course. I'd like to attend you all to a very beautiful model of computation called interaction nets. One application this model is used for is to optimally implement lambda calculus in a certain theoretical sense.
The paper I wrote connects the Post correspondence problem (PCP) to interaction nets, by reducing PCP in a number of steps to an interaction net and giving some suggestions for the other way around. (Thereby proving interaction nets at least Turing complete, and leaving the suggestion for Turing equivalence.)
The reverse proof is much more involved, needing multiple reduction steps, possibly through the chemical abstract machine I referenced.
I hope some of you will be inspired by interaction nets.
You can find the paper here.
The paper I wrote connects the Post correspondence problem (PCP) to interaction nets, by reducing PCP in a number of steps to an interaction net and giving some suggestions for the other way around. (Thereby proving interaction nets at least Turing complete, and leaving the suggestion for Turing equivalence.)
The reverse proof is much more involved, needing multiple reduction steps, possibly through the chemical abstract machine I referenced.
I hope some of you will be inspired by interaction nets.
You can find the paper here.
Slides Church-Turing Thesis and Gödels Incompleteness Theorems
A pair of slides this time. Again for Models of Computation I held a presentation, this time about the Church-Turing Thesis and some interesting variants of it. As a computer scientist one should really know the general ideas surrounding it.
And finally slides for a Philosophy of AI course about Gödel's Incompleteness Theorems (mostly the first theorem). In the slides I tackle some possible misconceptions when interpreting the theorem and try to convince you that Gödel's Incompleteness Theorems, although very interesting, are not very usable in a philosophical argument, but can be used as a starting point for devising new philosophical theories.
I hope you'll find it interesting and comments are always welcome.
The slides for the Church-Turing Thesis can be downloaded here.
The slides for Gödel's Incompleteness Theorems can be downloaded here.
Slides Church-Turing Thesis (MoC)
Slides Gödels Incompleteness Theorems
The slides for the Church-Turing Thesis can be downloaded here.
The slides for Gödel's Incompleteness Theorems can be downloaded here.
And finally slides for a Philosophy of AI course about Gödel's Incompleteness Theorems (mostly the first theorem). In the slides I tackle some possible misconceptions when interpreting the theorem and try to convince you that Gödel's Incompleteness Theorems, although very interesting, are not very usable in a philosophical argument, but can be used as a starting point for devising new philosophical theories.
I hope you'll find it interesting and comments are always welcome.
The slides for the Church-Turing Thesis can be downloaded here.
The slides for Gödel's Incompleteness Theorems can be downloaded here.
Slides Church-Turing Thesis (MoC)
Slides Gödels Incompleteness Theorems
The slides for the Church-Turing Thesis can be downloaded here.
The slides for Gödel's Incompleteness Theorems can be downloaded here.
Tuesday, 18 May 2010
Post's Correspondence Problem
So I held a presentation for my course Models of Computation and I thought I'd share the slides with you.
The presentation is about the classic recursively unsolvable problem called Post's Correspondence Problem. I hope you find it interesting.
Slides MoC
Updated:
You can get the slides here.
I now completed the course and completed a paper related to this presentation. You can find that here.
The presentation is about the classic recursively unsolvable problem called Post's Correspondence Problem. I hope you find it interesting.
Slides MoC
Updated:
You can get the slides here.
I now completed the course and completed a paper related to this presentation. You can find that here.
Wednesday, 7 April 2010
A small handout on TTTAS (Typed Transformations of Typed Abstract Syntax)
This period I did the course Advanced Functional Programming and I had to choose a subject from a set list of subjects to present. I chose typed transformations of typed abstract syntax (TTTAS). (See this webpage for the technical report and associated library by Arthur Baars, Doaitse Swierstra and Marcos Viera.)
I already expected the subject to be one of the harder ones and I also had a restriction for the presentation due to practical issues, namely we could only use handouts (or your own laptop) and not a beamer because of multiple presenters.
Thus I made some handouts in a tutorial like fashion. It might save you some typing of the code found in the paper and hopefully get you interested in the subject. You might also find it useful to get some motivation for the use of GADTs and transformations of EDSLs in general.
The handouts:
The PDF file is here.
The lhs can be found here.
I already expected the subject to be one of the harder ones and I also had a restriction for the presentation due to practical issues, namely we could only use handouts (or your own laptop) and not a beamer because of multiple presenters.
Thus I made some handouts in a tutorial like fashion. It might save you some typing of the code found in the paper and hopefully get you interested in the subject. You might also find it useful to get some motivation for the use of GADTs and transformations of EDSLs in general.
The handouts:
The PDF file is here.
The lhs can be found here.
Sunday, 10 January 2010
Using LaTeX for homework exercises
Last period I had a course about development of knowledge systems for which I had to do weekly (and quite large) assignments. The assignments were more suited for information science majors and therefore easier on the technical side. So I found this a good opportunity to invest some time in learning some more LaTeX by doing (most of) the exercises in LaTeX.
Anyway, one of the problems I had while working with LaTeX was the lack of larger examples. The documentation for LaTeX and the packages I used was pretty good most of the times, but larger examples still help a lot when you're just starting out. So hoping some people will get use out of it, I've uploaded the sources of my solutions to the exercises. (Of course these solutions are not 100% correct.)
Some of the packages I used were amsmath and amssymb. These really helped a lot to do the proofs. (Some documentation can be found here and here.)
For Assignment 2 I also learned to use graphviz to draw my graphs. So some example DOT files are included in the extras. (The guide I used was here.)
I split the assignments into the original problem description (the part I had to deliver was the hand-in part), the LaTeX source and other sources such as pictures, the final outputted PDF and possibly additional sources such as the solutions in the tools.
Assignment 1 (Logic):
Problem description | LaTeX + other source files | Outputted PDF | Extra files
(Extra files include the python files I used and edited to generate the truth tables in LaTeX, thanks to midorikid)
Assignment 2 (CLIPS):
Problem description | LaTeX + other source files | Outputted PDF | Extra files | CLIPS
(Extra files include the DOT files I used for graphviz, Microsoft Visio Drawing of the family tree and the CLIPS files I made.)
Assignment 3 (Protégé):
This was not done in LaTeX because I did not have access to my own computer. If you're interested, tell me, and I'll find the sources from Protégé and Microsoft Word anyway.
Assignment 4 (Hugin/Probability Theory):
Problem description | LaTeX + other source files | Outputted PDF | Extra files | Hugin
(Extra files include the multiple probabilistic networks.)
Assignment 5 (Fuzzy Logic/Systems):
Problem description | LaTeX + other source files | Outputted PDF | Extra files
(Extra files include the Maple 13 file to model the functions.)
Anyway, one of the problems I had while working with LaTeX was the lack of larger examples. The documentation for LaTeX and the packages I used was pretty good most of the times, but larger examples still help a lot when you're just starting out. So hoping some people will get use out of it, I've uploaded the sources of my solutions to the exercises. (Of course these solutions are not 100% correct.)
Some of the packages I used were amsmath and amssymb. These really helped a lot to do the proofs. (Some documentation can be found here and here.)
For Assignment 2 I also learned to use graphviz to draw my graphs. So some example DOT files are included in the extras. (The guide I used was here.)
I split the assignments into the original problem description (the part I had to deliver was the hand-in part), the LaTeX source and other sources such as pictures, the final outputted PDF and possibly additional sources such as the solutions in the tools.
Assignment 1 (Logic):
Problem description | LaTeX + other source files | Outputted PDF | Extra files
(Extra files include the python files I used and edited to generate the truth tables in LaTeX, thanks to midorikid)
Assignment 2 (CLIPS):
Problem description | LaTeX + other source files | Outputted PDF | Extra files | CLIPS
(Extra files include the DOT files I used for graphviz, Microsoft Visio Drawing of the family tree and the CLIPS files I made.)
Assignment 3 (Protégé):
This was not done in LaTeX because I did not have access to my own computer. If you're interested, tell me, and I'll find the sources from Protégé and Microsoft Word anyway.
Assignment 4 (Hugin/Probability Theory):
Problem description | LaTeX + other source files | Outputted PDF | Extra files | Hugin
(Extra files include the multiple probabilistic networks.)
Assignment 5 (Fuzzy Logic/Systems):
Problem description | LaTeX + other source files | Outputted PDF | Extra files
(Extra files include the Maple 13 file to model the functions.)
Wednesday, 4 November 2009
Comparing Parser Construction Techniques
Already a few months ago I completed my Bachelor computer science by writing a small paper and attending and presenting at a student conference. Well anyway, the topic I wrote about is parser construction techniques. The paper talks about parser generators (ANTLR in specific), parser combinators (Parsec 2) and a nice novel combination of the two (Tinadic Parsing, still to published somewhere in the future).
Anyway I hope this paper might be interesting to some people reading my blog. The paper comes with quite some code examples and it's probably not a very hard read. So you might consider it a small tutorial on parser construction techniques (or even learn some Parsec while you're at it :) ).
My paper can be found here at the website of the University of Twente.
The accompanying code examples can be found here. If someone would really appreciate it, I might consider writing some more documentation.
As you might have noticed blog posts were a bit scarce the last weeks, because of my silly ambition of taking 3 instead of 2 courses :P. Anyway, I'm liking the pace but my side activities suffer a bit, so I'll probably switch back after next period.
(People waiting for the extended state monad implementation: I haven't given up yet!)
Anyway I hope this paper might be interesting to some people reading my blog. The paper comes with quite some code examples and it's probably not a very hard read. So you might consider it a small tutorial on parser construction techniques (or even learn some Parsec while you're at it :) ).
My paper can be found here at the website of the University of Twente.
The accompanying code examples can be found here. If someone would really appreciate it, I might consider writing some more documentation.
As you might have noticed blog posts were a bit scarce the last weeks, because of my silly ambition of taking 3 instead of 2 courses :P. Anyway, I'm liking the pace but my side activities suffer a bit, so I'll probably switch back after next period.
(People waiting for the extended state monad implementation: I haven't given up yet!)
Subscribe to:
Posts (Atom)
