headers
Sebastian Hanowski | 8 Aug 2006 13:33
Picon

Re: [ANNOUNCE] A type-correct n : Val T

* Am 21.07.06 schrieb Joel Wright:
> Hi Everyone,
> 
> It is my pleasure to announce the immediate availability of a
> Functional Pearl entitled "A type-correct, stack-safe, provably
> correct, expression compiler in Epigram", which will shortly be
> submitted to the Journal of Functional Programming.
> 
> The abstract is included below, and the full paper and program source
> can be found at "http://www.cs.nott.ac.uk/~jjw" (also on
> "http://www.e-pig.org/" soon).
> 
> We hope you enjoy it,
> Joel Wright and James McKinna.
> 
> ----------------
> --- ABSTRACT ---
> ----------------
> 
> Conventional approaches to compiler correctness, type safety and type
> preservation have focused on off-line proofs, either on paper or
> formalised with a machine, of existing compilation schemes with
> respect to a reference operational semantics. This pearl shows how the
> use of dependent types in programming, illustrated here in Epigram,
> allows us not only to build-in these properties, but to write programs
> which guarantee them by design and subsequent construction.
> 
> We focus here on a very simple expression language, compiled into
> tree-structured code for a simple stack machine. Our purpose here is
> not to claim any sophistication in the source language being modelled,
(Continue reading)

Permalink | Reply | 0 comments |
headers
Wolfgang Jeltsch | 10 Aug 2006 23:28

Re: defining terms

Am Montag, 27. Februar 2006 11:33 schrieb Conor McBride:
> [...]

> Wolfgang Jeltsch wrote:
> [...]

> >While we are at contributions: In which way could a beginning postgraduate
> > who is very much interested in Epigram contribute to it?  I'm currently
> > employed as a teaching assistant at the Brandenburg University of
> > Technology at Cottbus, Germany and want/need to create a PhD thesis.  My
> > professor gave me certain freedom in choosing the topic of my thesis.  So
> > I asked him if something about Epigram would be in his interest and he
> > told me that he is principally open for such a topic.
>
> This is a very good and timely question. There are lots of things to
> think about, most of which go 'how should we treat feature X in
> Epigram?', which tends to decompose into three parts 'how should feature
> X appear to the programmer?', 'how do we model feature X in our type
> theory (extending it if necessary)?' and 'how might the elaborator get
> from one to the other?'. And possibly a fourth 'what has become easy
> which was hard before?'. There's a large collection of candidates for
> feature X, plenty enough to share around: polymorphic stratified
> universes, coinduction, IO, the Partial monad, monads and other notions
> of computation generally, induction-recursion, datatype refinement,
> reflection, generic programming, program specification and derivation,
> linearity, quotients, modules, I could go on and I'm sure others could
> too...

Oh dear, it seems that it took me almost half a year to answer this e-mail.  
(But this doesn't mean that I was sleeping during this time.  For example, I
(Continue reading)

Permalink | Reply | 1 comment |
headers
Sebastian Hanowski | 12 Aug 2006 13:51
Picon

lib-service

* Am 10.08.06 schrieb Wolfgang Jeltsch:
> Am Montag, 27. Februar 2006 11:33 schrieb Conor McBride:
> > which was  hard before?'. There's  a large collection  of candidates
> > for  feature   X,  plenty   enough  to  share   around:  polymorphic
> > stratified   universes[1],   coinduction[2],  IO[3],   the   Partial
> > monad[4],  monads and  other  notions  of computation  generally[5],
> > induction-recursion[6],   datatype   refinement[7],   reflection[8],
> > generic  programming[9], program  specification and  derivation[10],
> > linearity[11],  quotients[12], modules[13],  I could  go on  and I'm
> > sure others could too...

> What  interests  me   know  is  whether  you  or   some  other  person
> could  recommend  me certain  papers  or  whatever which  explain  the
> above-mentioned topics  to some  degree, give  background information,
> state the state of the art, etc. For example, I currently have no clue

A few picks form my bookmarks tagged 'toread' if not to say
'tounderstand':

[1]
http://www.mail-archive.com/epigram <at> durham.ac.uk/msg00213.html
http://www.cs.nott.ac.uk/~txa/oxford04/
http://sneezy.cs.nott.ac.uk/epigram/durham/examples/ctm/veczip.epi

[2]
http://www.cs.nott.ac.uk/~gmh/corecursion.pdf

[3]     
http://www.haskell.org/tutorial/io.html
(Continue reading)

Permalink | Reply | 0 comments |
headers
Sebastian Hanowski | 17 Aug 2006 19:27
Picon

how to view backwards without crashing your program

 Issues of replacing constrain-by-instantiation by constrain-by-equation
for   datatype   declarations    in   Sec.   5   of    the   OTT   paper
http://www.cs.nott.ac.uk/~txa/publ/ott-conf.pdf let me  revert to an old
vice of mine, that is to  constrain computations by equation in Epigram.
Where the first  is used to put focus on  unfocused families, the latter
let's the typechecker work even harder for you.

 For example,  subtraction on  the naturals requires  only less  then or
equal numbers to be substracted. You can assure this to the typechecker
by  passing an  argument which  is an  inductive proof  that the  second
number is less  then or equal to  the first. One can find  this in Edwin
Brady's thesis http://www.dcs.st-andrews.ac.uk/~eb/writings/thesis.pdf .
This also gives an additional possibility for recursion.

But one can also give this precondition by an equation:

------------------------------------------------------------------------------
                                       (  n : Nat   !
data (---------!  where (---------! ;  !------------!
     ! Nat : * )        ! O : Nat )    ! |+ n : Nat )
------------------------------------------------------------------------------
     (   m, n : Nat   !                
let  !----------------!                
     ! plus m n : Nat )                

     plus m n <= rec m                 
     { plus m n <= case m              
       { plus O n => n                 
         plus (|+ m) n => |+ (plus m n)
       }
(Continue reading)

Permalink | Reply | 0 comments |

Gmane