https://www.bibsonomy.org/user/draganigajic/mlBibSonomy RSS Feed for /user/draganigajic/mlhttp://www-db.stanford.edu/~ullman/draganigajic2011-07-13T18:13:40+02:00People cs db ml pl research <a itemprop="url" data-versiondate="2011-07-13T18:13:40+02:00" href="http://www-db.stanford.edu/~ullman/" rel="nofollow" class="description-link">http://www-db.stanford.edu/~ullman/</a>http://www.laserpirate.com/tinyml.htmldraganigajic2011-07-13T18:13:38+02:00ml <a itemprop="url" data-versiondate="2011-07-13T18:13:38+02:00" href="http://www.laserpirate.com/tinyml.html" rel="nofollow" class="description-link">http://www.laserpirate.com/tinyml.html</a>http://mlton.org/SyntacticConventionsdraganigajic2011-07-13T18:13:30+02:00ml <a itemprop="url" data-versiondate="2011-07-13T18:13:30+02:00" href="http://mlton.org/SyntacticConventions" rel="nofollow" class="description-link">http://mlton.org/SyntacticConventions</a>v coolhttp://www.macs.hw.ac.uk/ultra/compositional-analysis/type-error-slicing/slicing.cgidraganigajic2011-07-13T18:13:18+02:00! cs demo ml programming typeTheory <span itemprop="description">v cool</span>http://mlton.org/FunctionalRecordUpdatedraganigajic2011-07-13T18:13:16+02:00algorithms fp ml sml <a itemprop="url" data-versiondate="2011-07-13T18:13:16+02:00" href="http://mlton.org/FunctionalRecordUpdate" rel="nofollow" class="description-link">http://mlton.org/FunctionalRecordUpdate</a>http://mlton.org/Featuresdraganigajic2011-07-13T18:13:16+02:00compiler features ml programming sml <a itemprop="url" data-versiondate="2011-07-13T18:13:16+02:00" href="http://mlton.org/Features" rel="nofollow" class="description-link">http://mlton.org/Features</a>http://en.wikipedia.org/wiki/Twelfdraganigajic2011-07-13T18:13:11+02:00cs logic ml proof twelf wikipedia <a itemprop="url" data-versiondate="2011-07-13T18:13:11+02:00" href="http://en.wikipedia.org/wiki/Twelf" rel="nofollow" class="description-link">http://en.wikipedia.org/wiki/Twelf</a>http://www.mpi-sws.mpg.de/~rossberg/mixml/draganigajic2011-07-13T18:13:10+02:00ml modules papers <a itemprop="url" data-versiondate="2011-07-13T18:13:10+02:00" href="http://www.mpi-sws.mpg.de/~rossberg/mixml/" rel="nofollow" class="description-link">http://www.mpi-sws.mpg.de/~rossberg/mixml/</a>http://twelf.plparty.org/wiki/Main_Pagedraganigajic2011-07-13T18:13:06+02:00cs deduction fp logic math ml pl proof twelf wiki <a itemprop="url" data-versiondate="2011-07-13T18:13:06+02:00" href="http://twelf.plparty.org/wiki/Main_Page" rel="nofollow" class="description-link">http://twelf.plparty.org/wiki/Main_Page</a>http://www.cis.upenn.edu/~bcpierce/draganigajic2011-07-13T18:13:05+02:00*RIL *read bibliography bidirectional categoryTheory coq cs fp haskell lectures logic ml people pl research sync teaching typeTheory unison upenn xml <a itemprop="url" data-versiondate="2011-07-13T18:13:05+02:00" href="http://www.cis.upenn.edu/~bcpierce/" rel="nofollow" class="description-link">http://www.cis.upenn.edu/~bcpierce/</a>http://lambda-the-ultimate.org/node/2920draganigajic2011-07-13T18:12:50+02:00algorithms announce ltu ml oz scheme <a itemprop="url" data-versiondate="2011-07-13T18:12:50+02:00" href="http://lambda-the-ultimate.org/node/2920" rel="nofollow" class="description-link">http://lambda-the-ultimate.org/node/2920</a>http://www.cs.rice.edu/~taha/draganigajic2011-07-13T18:12:50+02:00cs fp metaprogramming ml ocaml people pl research <a itemprop="url" data-versiondate="2011-07-13T18:12:50+02:00" href="http://www.cs.rice.edu/~taha/" rel="nofollow" class="description-link">http://www.cs.rice.edu/~taha/</a>http://research.microsoft.com/~minka/papers/draganigajic2011-07-13T18:12:25+02:00bayesian bibliography machinelearning ml people research statistics <a itemprop="url" data-versiondate="2011-07-13T18:12:25+02:00" href="http://research.microsoft.com/~minka/papers/" rel="nofollow" class="description-link">http://research.microsoft.com/~minka/papers/</a>Standard ML is often used to implement another language L, for example, the syntax of the HOL logic in hol90 or the syntax of CCS for the Concurrency Workbench. Typically, one defines the abstract syntax of L by a datatype declaration. Then useful functions over the datatype can be defined (such as finding the free variables of a formula when L is a logic). Soon afterwards, one concludes that concrete syntax is easier for humans to read than abstract syntax, and so writes a parser and prettyprinter for L. In the situation just outlined, ML is called the metalanguage, and L is called the object language, or OL. (Edinburgh/INRIA/Cambridge ML, the precursor to Standard ML, was originally a programming metalanguage for a particular object language, the LCF logic.) The purpose of a quotation/antiquotation mechanism is to allow one to embed expressions in the object language's concrete syntax inside of ML programs, and to mix the object language expressions with ML expressions.http://www.smlnj.org//doc/quote.htmldraganigajic2011-07-13T18:12:21+02:00metaprogramming ml sml <span itemprop="description">Standard ML is often used to implement another language L, for example, the syntax of the HOL logic in hol90 or the syntax of CCS for the Concurrency Workbench. Typically, one defines the abstract syntax of L by a datatype declaration. Then useful functions over the datatype can be defined (such as finding the free variables of a formula when L is a logic). Soon afterwards, one concludes that concrete syntax is easier for humans to read than abstract syntax, and so writes a parser and prettyprinter for L. In the situation just outlined, ML is called the metalanguage, and L is called the object language, or OL. (Edinburgh/INRIA/Cambridge ML, the precursor to Standard ML, was originally a programming metalanguage for a particular object language, the LCF logic.) The purpose of a quotation/antiquotation mechanism is to allow one to embed expressions in the object language&#039;s concrete syntax inside of ML programs, and to mix the object language expressions with ML expressions.</span>http://cs.hubfs.net/forums/default.aspxdraganigajic2011-07-13T18:12:18+02:00community dotnet f# forum ml programming <a itemprop="url" data-versiondate="2011-07-13T18:12:18+02:00" href="http://cs.hubfs.net/forums/default.aspx" rel="nofollow" class="description-link">http://cs.hubfs.net/forums/default.aspx</a>Tim Sheard, Zine-el-abidine Benaissa, and Emir Pasalic * Introduction * Staging in MetaML * Monads in Langauge Design * Monads in METAML * Illustrating our compiler development method o The while-language o The structure of the solution o Step 1: monadic interpreter o Step 2: staged interpreter + Interpreter for Commands. + An example. * Step 3: Back-end translation and intermediate code optimization o Intensional analysis of code fragmentshttp://www.usenix.org/events/dsl99/full_papers/sheard/sheard_html/dsl.htmldraganigajic2011-07-13T18:12:18+02:00compiler dsl metaml ml paper usenix <span itemprop="description">Tim Sheard, Zine-el-abidine Benaissa, and Emir Pasalic * Introduction * Staging in MetaML * Monads in Langauge Design * Monads in METAML * Illustrating our compiler development method o The while-language o The structure of the solution o Step 1: monadic interpreter o Step 2: staged interpreter + Interpreter for Commands. + An example. * Step 3: Back-end translation and intermediate code optimization o Intensional analysis of code fragments</span>http://www.ps.uni-sb.de/alice/manual/tour.htmldraganigajic2011-07-13T18:12:18+02:00alice concurrency dataflow distributed ml oz tutorial <a itemprop="url" data-versiondate="2011-07-13T18:12:18+02:00" href="http://www.ps.uni-sb.de/alice/manual/tour.html" rel="nofollow" class="description-link">http://www.ps.uni-sb.de/alice/manual/tour.html</a>we develop an approach for reconciling open programming -- the development of programs that support dynamic exchange of higher-order values with strong static typing. conventional functional language extended with a set of orthogonal features like higher-order modules, dynamic type checking, higher-order serialisation, and concurrency. On top of these a flexible system of dynamic components and a simple but expressive notion of distribution is realised. The central concept in this design is the packag}, a first-class value embedding a module along with its interface type. formal model for abstract types that is not invalidated by the presence of primitives for dynamic type inspection, as is the case for the standard model based on existential quantification. For that we present an idealised language in form of an extended lambda-calculus, which can express dynamic generation of types.http://www.ps.uni-sb.de/Papers/abstracts/top.htmldraganigajic2011-07-13T18:12:18+02:00alice ml paper pdf thesis <span itemprop="description">we develop an approach for reconciling open programming -- the development of programs that support dynamic exchange of higher-order values with strong static typing. conventional functional language extended with a set of orthogonal features like higher-order modules, dynamic type checking, higher-order serialisation, and concurrency. On top of these a flexible system of dynamic components and a simple but expressive notion of distribution is realised. The central concept in this design is the packag}, a first-class value embedding a module along with its interface type. formal model for abstract types that is not invalidated by the presence of primitives for dynamic type inspection, as is the case for the standard model based on existential quantification. For that we present an idealised language in form of an extended lambda-calculus, which can express dynamic generation of types.</span>We introduce a new lambda calculus with futures, Lambda(fut), that models the operational semantics of concurrent statically typed functional programming languages with mixed eager and lazy threads such as Alice ML, a concurrent extension of Standard ML. Lambda(fut) is a minimalist extension of the call-by-value lambda-calculus that is sufficiently expressive to define and combine a variety of standard concurrency abstractions, such as channels, semaphores, and ports. Despite its minimality, the basic machinery of Lambda(fut) is sufficiently powerful to support explicit recursion and call-by-need evaluation. We present a static type system for Lambda(fut) and distinguish a fragment of Lambda(fut) that we prove to be uniformly confluent. This result confirms our intuition that reference cells are the sole source of indeterminism.http://www.ps.uni-sb.de/Papers/paper_info.php?label=jlambda-futdraganigajic2011-07-13T18:12:18+02:00alice concurrency cs fp lambdacalculus ml paper pdf <span itemprop="description">We introduce a new lambda calculus with futures, Lambda(fut), that models the operational semantics of concurrent statically typed functional programming languages with mixed eager and lazy threads such as Alice ML, a concurrent extension of Standard ML. Lambda(fut) is a minimalist extension of the call-by-value lambda-calculus that is sufficiently expressive to define and combine a variety of standard concurrency abstractions, such as channels, semaphores, and ports. Despite its minimality, the basic machinery of Lambda(fut) is sufficiently powerful to support explicit recursion and call-by-need evaluation. We present a static type system for Lambda(fut) and distinguish a fragment of Lambda(fut) that we prove to be uniformly confluent. This result confirms our intuition that reference cells are the sole source of indeterminism.</span>Despite its powerful module system, ML has not yet evolved for the modern world of dynamic and open modular programming, to which more primitive languages have adapted better so far. We present the design and semantics of a simple yet expressive first-class component system for ML. It provides dynamic linking in a type-safe and type-flexible manner, and allows selective execution in sandboxes. The system is defined solely by reduction to higher-order modules plus an extension with simple module-level dynamics, which we call packages. To represent components outside processes we employ generic pickling. We give a module calculus formalising the semantics of packages and pickling.http://www.ps.uni-sb.de/Papers/abstracts/missing-link-extended.htmldraganigajic2011-07-13T18:12:18+02:00alice cs distributed ml modules paper pdf <span itemprop="description">Despite its powerful module system, ML has not yet evolved for the modern world of dynamic and open modular programming, to which more primitive languages have adapted better so far. We present the design and semantics of a simple yet expressive first-class component system for ML. It provides dynamic linking in a type-safe and type-flexible manner, and allows selective execution in sandboxes. The system is defined solely by reduction to higher-order modules plus an extension with simple module-level dynamics, which we call packages. To represent components outside processes we employ generic pickling. We give a module calculus formalising the semantics of packages and pickling.</span>