@INPROCEEDINGS{Stegeman14:codequality,
AUTHOR = {Stegeman, Martijn and Barendsen, Erik and Smetsers, Sjaak},
TITLE = {Towards an Empirically Validated Model for Assessment of Code Quality},
BOOKTITLE = {Proceedings of the 14th Koli Calling International Conference on Computing Education Research},
SERIES = {Koli Calling '14},
YEAR = {2014},
ISBN = {978-1-4503-3065-7},
LOCATION = {Koli, Finland},
PAGES = {99--108},
NUMPAGES = {10},
PUBLISHER = {ACM},
ADDRESS = {New York, NY, USA},
KEYWORDS = {assessment, code quality, empirical validation, feedback, programming education, rubrics}
}
@INCOLLECTION{Bernstein15:TweetNaCl,
YEAR = {2015},
ISBN = {978-3-319-16294-2},
BOOKTITLE = {Progress in Cryptology - LATINCRYPT 2014},
VOLUME = {8895},
SERIES = {Lecture Notes in Computer Science},
EDITOR = {Aranha, Diego F. and Menezes, Alfred},
DOI = {10.1007/978-3-319-16295-9_4},
TITLE = {TweetNaCl: A Crypto Library in 100 Tweets},
URL = {http://dx.doi.org/10.1007/978-3-319-16295-9_4},
PUBLISHER = {Springer International Publishing},
KEYWORDS = {Trusted code base; Source-code size; Auditability; Software implementation; Timing-attack protection; NaCl; Twitter},
AUTHOR = {Bernstein, DanielJ. and van Gastel, Bernard and Janssen, Wesley and Lange, Tanja and Schwabe, Peter and Smetsers, Sjaak},
PAGES = {64-83},
LANGUAGE = {English}
}
@INPROCEEDINGS{Madlener13sblp,
AUTHOR = {{Madlener}, Ken and {Smetsers}, Sjaak and {van Eekelen}, Marko},
TITLE = {Modular bialgebraic semantics and algebraic laws},
BOOKTITLE = {Proceedings of SBLP'13},
PAGES = {46--60},
PUBLISHER = {LNCS},
VOLUME = {8129},
YEAR = {2013}
}
@INPROCEEDINGS{Madlener13tase,
AUTHOR = {Ken Madlener and Sjaak Smetsers},
TITLE = {{GSOS} Formalized in {C}oq},
BOOKTITLE = {Proceedings of TASE'13},
PAGES = {199--206},
PUBLISHER = {IEEE},
YEAR = {2013}
}
@INPROCEEDINGS{Smetsers13BFC,
AUTHOR = {Sjaak Smetsers and
Erik Barendsen},
TITLE = {Verifying Functional Formalizations - A type-theoretical case study in PVS},
BOOKTITLE = {The Beauty of Functional Code},
PAGES = {47-59},
EE = {http://dx.doi.org/10.1007/978-3-642-40355-2_1},
EDITOR = {Peter Achten and
Pieter W. M. Koopman},
PUBLISHER = SPRINGER,
SERIES = LNCS,
VOLUME = {8106},
YEAR = {2013},
ISBN = {978-3-642-40354-5},
EE = {http://dx.doi.org/10.1007/978-3-642-40355-2},
CLASS = {Wet}
}
@INPROCEEDINGS{KerstenNFM13,
AUTHOR = {Rody Kersten and Bernard van Gastel and Manu Drijvers and Sjaak Smetsers and Marko van Eekelen},
BOOKTITLE = {Proceedings of the 5th NASA Formal Methods Symposium.},
EDITOR = {G. Brat and N. Rungta and A. Venet},
MONTH = {May},
NUMBER = {7871},
PUBLISHER = {Springer},
PAGES = {63--77},
SERIES = {Lecture Notes in Computer Science},
TITLE = {Using Model-Checking to Reveal a Vulnerability of Tamper-Evident Pairing},
YEAR = {2013}
}
@TECHREPORT{Madlener13-TR,
AUTHOR = {{Madlener}, Ken and {Smetsers}, Sjaak and {van Eekelen}, Marko},
TITLE = {{Modular bialgebraic semantics and algebraic laws}},
NUMBER = {ICIS--R13008},
MONTH = {July},
INSTITUTION = {Radboud University Nijmegen},
YEAR = {2013},
RESEARCH_GROUP = {ds},
CLASS = {Report}
}
@INPROCEEDINGS{Smetsers13,
YEAR = {2013},
ISBN = {978-3-642-40446-7},
BOOKTITLE = {Trends in Functional Programming},
VOLUME = {7829},
SERIES = {Lecture Notes in Computer Science},
EDITOR = {Loidl, Hans-Wolfgang and Peña, Ricardo},
DOI = {10.1007/978-3-642-40447-4_6},
TITLE = {Higher-Order Strictness Typing},
URL = {http://dx.doi.org/10.1007/978-3-642-40447-4_6},
PUBLISHER = {Springer Berlin Heidelberg},
AUTHOR = {Smetsers, Sjaak and van Eekelen, Marko},
PAGES = {85-100},
LANGUAGE = {English}
}
@INPROCEEDINGS{DBLP:conf/ifm/LensinkSE12,
AUTHOR = {Leonard Lensink and
Sjaak Smetsers and
Marko C. J. D. van Eekelen},
TITLE = {A Proof Framework for Concurrent Programs},
BOOKTITLE = {IFM},
YEAR = {2012},
PAGES = {174-190},
EE = {http://dx.doi.org/10.1007/978-3-642-30729-4_13},
CROSSREF = {DBLP:conf/ifm/2012},
BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}
@PROCEEDINGS{DBLP:conf/ifm/2012,
EDITOR = {John Derrick and
Stefania Gnesi and
Diego Latella and
Helen Treharne},
TITLE = {Integrated Formal Methods - 9th International Conference,
IFM 2012, Pisa, Italy, June 18-21, 2012. Proceedings},
BOOKTITLE = {IFM},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {7321},
YEAR = {2012},
ISBN = {978-3-642-30728-7},
EE = {http://dx.doi.org/10.1007/978-3-642-30729-4},
BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}
@INPROCEEDINGS{DBLP:conf/nfm/LensinkSE12,
AUTHOR = {Leonard Lensink and
Sjaak Smetsers and
Marko C. J. D. van Eekelen},
TITLE = {Generating Verifiable Java Code from Verified PVS Specifications},
BOOKTITLE = {NASA Formal Methods},
YEAR = {2012},
PAGES = {310-325},
EE = {http://dx.doi.org/10.1007/978-3-642-28891-3_30},
CROSSREF = {DBLP:conf/nfm/2012},
BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}
@PROCEEDINGS{DBLP:conf/nfm/2012,
EDITOR = {Alwyn Goodloe and
Suzette Person},
TITLE = {NASA Formal Methods - 4th International Symposium, NFM 2012,
Norfolk, VA, USA, April 3-5, 2012. Proceedings},
BOOKTITLE = {NASA Formal Methods},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {7226},
YEAR = {2012},
ISBN = {978-3-642-28890-6},
EE = {http://dx.doi.org/10.1007/978-3-642-28891-3},
BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}
@INPROCEEDINGS{Madlener11,
AUTHOR = {Madlener, Ken and
Smetsers, Sjaak and
van Eekelen, Marko},
TITLE = {Formal Component-Based Semantics},
BOOKTITLE = {Proceedings of the 8th Workshop on Structural Operational Semantics (SOS'11)},
EDITOR = {Michel A. Reniers and Pawel Sobocinski},
YEAR = {2011},
PAGES = {17-29},
SERIES = {Electronic Proceedings in Theoretical Computer Science},
VOLUME = {62},
EE = {http://dx.doi.org/10.4204/EPTCS.62.2},
CROSSREF = {DBLP:journals/corr/abs-1108-2796},
BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}
@INCOLLECTION{Madlener10,
TITLE = {A formal verification study on the {R}otterdam storm surge barrier},
AUTHOR = {Madlener, Ken and Smetsers, Sjaak and van Eekelen, Marko},
BOOKTITLE = {Proceedings of the 12th International Conference on Formal Engineering Methods (IFCEM'10)},
EDITOR = {Jin Song Dong and Huibiao Zhu},
SERIES = {LNCS},
VOLUME = {6447},
PAGES = {287--302},
YEAR = {2010},
PUBLISHER = {Springer}
}
@INPROCEEDINGS{DBLP:conf/fmics/LensinkSE07,
AUTHOR = {Leonard Lensink and
Sjaak Smetsers and
Marko C. J. D. van Eekelen},
TITLE = {Machine Checked Formal Proof of a Scheduling Protocol for
Smartcard Personalization},
BOOKTITLE = {FMICS},
YEAR = {2007},
PAGES = {115-132},
EE = {http://dx.doi.org/10.1007/978-3-540-79707-4_10},
CROSSREF = {DBLP:conf/fmics/2007},
BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}
@PROCEEDINGS{DBLP:conf/fmics/2007,
EDITOR = {Stefan Leue and
Pedro Merino},
TITLE = {Formal Methods for Industrial Critical Systems, 12th International
Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised
Selected Papers},
BOOKTITLE = {FMICS},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {4916},
YEAR = {2008},
ISBN = {978-3-540-79706-7},
BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}
@INPROCEEDINGS{Sme10,
AUTHOR = {Sjaak Smetsers},
TITLE = {The Syntactic Continuity Property: A computer verified proof},
BOOKTITLE = {International Conference on Theoretical and Mathematical Foundations of Computer Science (TMFCS10)},
PUBLISHER = {ISRST},
EDITOR = {Zoran Majkic, Sun-Yuan Hsieh Jixin Ma and Ibrahiem M M El Emary, Khalid S HusainEditors},
YEAR = {2010},
PAGES = {135--142},
LOCATION = {Orlando, FL, USA},
CLASS = WET
}
@INPROCEEDINGS{STTES_IPCModel_FMICS09,
AUTHOR = {Schierboom, Erik and Tamalet, Alejandro and Tews, Hendrik and
van Eekelen, Marko and Smetsers, Sjaak},
TITLE = {Preemption Abstraction: A Lightweight Approach to Modelling Concurrency},
BOOKTITLE = {Formal Methods for Industrial Critical Systems (FMICS 2009)},
PUBLISHER = SPRINGER,
SERIES = LNCS,
VOLUME = {5825},
YEAR = {2009},
ISBN = {978-3-642-04569-1},
PAGES = {149-164},
CLASS = {wet}
}
@ARTICLE{smet08:LaQuSo,
AUTHOR = {Smetsers, Sjaak and {Eekelen, van}, Marko},
TITLE = {LaQuSo: Using Formal Methods for Analysis, Verification and Improvement of Safety Critical Software.},
JOURNAL = {Quarterly Magazine of the European Research Consortium for Informatics and Mathematics. Special Theme Safety-Critical Software},
YEAR = {2008},
VOLUME = {75},
PAGES = {38--39},
MONTH = {October},
PUBLISHER = {ERCIM NEWS}
}
@ARTICLE{Smetsers:2009:ETG:1555004.1555114,
AUTHOR = {Smetsers, Sjaak and van Weelden, Arjen and Plasmeijer, Rinus},
TITLE = {Efficient and Type-Safe Generic Data Storage},
JOURNAL = {Electron. Notes Theor. Comput. Sci.},
ISSUE_DATE = {June, 2009},
VOLUME = {238},
NUMBER = {2},
MONTH = JUN,
YEAR = {2009},
ISSN = {1571-0661},
PAGES = {59--70},
NUMPAGES = {12},
ACMID = {1555114},
PUBLISHER = {Elsevier Science Publishers B. V.},
ADDRESS = {Amsterdam, The Netherlands, The Netherlands},
KEYWORDS = {Polytypic/generic programming, data storage/sequentialization, functional programming, type inference},
ABSTRACT = {In this paper we present an elegant method for sequentializing arbitrary data using the generic language extension of
the functional programming language Clean. We show how the proposed operations can be used to store values of any
concrete data type in several kinds of IO containers (such as files or arrays of characters), and how to manipulate
stored data efficiently. Moreover, by extending stored data with encoded type information, data manipulation will be
type-safe. Defining these operations generically has the advantage that specific instances for user defined data types
can be generated fully automatically. Compared to traditional sequentialization methods (or to common data
manipulation, using relational data bases) our operations are an order of magnitude faster.}
}
@TECHREPORT{2008-Smetsers-TheoryFormalizing,
AUTHOR = {{Smetsers}, Sjaak and {Barendsen}, Erik},
TITLE = {{Formalizing Type Theory in PVS: a case study}},
NUMBER = {ICIS--R08022},
MONTH = {December},
INSTITUTION = {Radboud University Nijmegen},
YEAR = {2008},
CODE = {icis.ICIS-R08022},
RESEARCH_GROUP = {ds},
CLASS = {Report},
ABSTRACT = {
In this case study we investigate the use of PVS for developing type theoretical concepts and verifying the correctness of a typing algorithm. PVS turns out to be very useful for efficient development of a sound basic theory about polymorphic typing. This research contributes to the PoplMark challenge on mechanizing metatheory.}
}
@TECHREPORT{2008-Plasmeijer-CombiningObject,
AUTHOR = {{Plasmeijer}, Rinus and {Smetsers}, Sjaak and {Weelden}, Arjen van},
TITLE = {{Interactive Combining of Typed Object Code}},
NUMBER = {ICIS--R08019},
MONTH = {November},
INSTITUTION = {Radboud University Nijmegen},
YEAR = {2008},
RESEARCH_GROUP = {ds},
CLASS = {Report},
ABSTRACT = {
The functional language Clean includes a hybrid type system: in addition to the traditional static type system it offers support for dynamically typed values, so called \emph{dynamics}. An expression of arbitrary static type can be packed into a dynamic, and via pattern matching on types a dynamic can be converted back to a value of statically known type. The most important aspect of dynamics is that they can be serialized, written to file, and exchanged between independently compiled applications in a type-safe way. Since dynamics may contain functions and closures, they can be regarded as type-safe plugins. An application can combine plugins in a type safe way to new ones, without having to know what the actual contents and types of the original plugins are. In this paper we explain the underlying implementation and the architecture of the run-time system needed to make this all possible. To show the expressive power of Clean`s dynamics we present an interactive shell, called Esther. The command line language of this shell provides the basic functionality of a strongly typed lazy functional language. Esther behaves like an interpreter (direct response) yet its resulting performance is comparable to compiled code. This is achieved by using the dynamic facility of Clean. The shell actually combines compiled code; no help from a compiler is needed. Moreover, type checking is for free using the run-time type unification of dynamics. In this way we have obtained a novel architectural framework in which one can freely mix functionality created by the compiler, functionality stored in dynamics by compiled applications, and functionality interactively created by using the shell command line interpreter.}
}
@INPROCEEDINGS{BarendsenHenk07,
AUTHOR = {Erik Barendsen and Sjaak Smetsers},
TITLE = {Strictness Analysis via Resource Typing},
BOOKTITLE = {Reflections on Type Theory, Lambda Calculus, and the Mind},
YEAR = {2007},
MONTH = {December},
ADDRESS = {Nijmegen, Netherlands},
PAGES = {29-40},
ABSTRACT = {
We present a new typing system for strictness analysis of functional
programs. The system extends standard typing (including recursive data types)
with strictness annotations and subtyping. Strictness typing is shown to be
sound with respect to a natural operational semantics. We demonstrate that
strictness types can be computed effectively.}
}
@INPROCEEDINGS{LensinkFMICS07,
AUTHOR = {Leonard Lensink and Sjaak Smetsers and Marko van Eekelen},
TITLE = {Machine Checked Formal Proof of a Scheduling Protocol for Smartcard Personalization},
YEAR = {2007},
BOOKTITLE = {12th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2007},
MONTH = {July},
ADDRESS = {Berlin, Germany},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
ABSTRACT = {
Using PVS (Prototype Verification System), we prove that an industry designed
scheduler for a smartcard personalization machine is safe and optimal.
This scheduler has previously been the subject of research in model checked scheduling synthesis
and verification. These verification and synthesis efforts have only been done for a limited
number of personalization stations. We have created an executable model and prove the scheduling
algorithm to be optimal and safe for any number of personalization stations.
This result shows that theorem provers can be successfully
used for industrial problems in cases where model checkers suffer from state explosion.}
}
@ARTICLE{JacobsFAC06,
AUTHOR = {Bart Jacobs and
Sjaak Smetsers and
Ronny Wichers Schreur},
TITLE = {Code-carrying theories},
JOURNAL = {Formal Asp. Comput.},
VOLUME = {19},
NUMBER = {2},
YEAR = {2007},
PAGES = {191-203},
EE = {http://dx.doi.org/10.1007/s00165-006-0013-4},
ABSTRACT = {
This paper is both a position paper on a particular approach in program correctness, and also a
contribution to this area. The approach entails the generation of programs (code) from the
executable content of logical theories. This capability already exists within the main theorem
provers like Coq, Isabelle and ACL2 and PVS. Here we will focus on issues portraying the use of
this methodology, rather than the underlying theory. We illustrate the power of the approach within
PVS via two case studies (on unification and compression) that lead to actual running code. We also
demonstrate its flexibility by extending the program generation capabilities. This paper fits in a
line of ongoing integration of programming and proving.}
}
@MISC{SmetsersUNIF06,
AUTHOR = {Sjaak Smetsers and Arjen van Weelden},
TITLE = {Bracket-abstraction Preserves Typability: A formal proof of {Diller-algorithm-C} in {PVS}},
HOWPUBLISHED = {UNIF 2006},
YEAR = {2006},
MONTH = {August},
ADDRESS = {Seattle, USA},
ABSTRACT = {
Bracket abstraction is an algorithm that transforms lambda
expressions into combinator terms. There are several versions of this algorithm
depending on the actual set of combinators that is used. Most
of them have been proven correct with respect to the operational semantics.
In this paper we focus on typability. We present a fully machine
verified proof of the property that bracket abstraction preserves types;
the types assigned to an expression before and after performing bracket
abstraction are identical. To our knowledge, this is the first time that
(1) such proof has been given, and (2) the proof is verified by a theorem
prover. The theorem prover used in the development of the proof is PVS.}
}
@INPROCEEDINGS{WeeldenIFL05,
AUTHOR = {Arjen van Weelden and Sjaak Smetsers and Rinus Plasmeijer},
TITLE = {Polytypic Syntax Tree Operations},
YEAR = {2005},
BOOKTITLE = {Implementation and Application of Functional Languages, 17th International Workshop, IFL 2005, Revised Selected Papers},
MONTH = {September},
ADDRESS = {Dublin, Ireland},
PUBLISHER = {Springer},
SERIES = {Lecture Notes in Computer Science},
ABSTRACT = {
Polytypic functional programming has the advantage that it can
derive code for generic functions automatically. However, it is not
clear whether it is useful for anything other than the textbook
examples, and the generated polytypic code is usually too slow for
real-life programs. As a real-life test, we derive a polytypic
parser for the Haskell 98 syntax and look into other front-end
compiler syntax tree operations. We present a types--as--grammar
approach, which uses polytypic programming (in both Generic Haskell
and Clean) to automatically derive the code for a parser based on
the syntax tree type, without using external tools. Moreover, we
show that using polytypic programming can even be useful for
data--specific syntax tree operations in a (functional) compiler,
such as scope checking and type inference. Simple speed tests show
that the performance of polytypic parsers can be abominable for
real-life inputs. However, we show that much performance can be
recovered by applying (extended) fusion optimization on the
generated code. We actually have a derived parser whose speed is
close to one generated by a specialized Haskell parser generator.}
}
@INPROCEEDINGS{AlimarineHW05,
AUTHOR = {Artem Alimarine and Sjaak Smetsers and Arjen van Weelden
and Marko van Eekelen and Rinus Plasmeijer},
TITLE = {There and Back Again: Arrows for Invertible Programming},
BOOKTITLE = {Proceedings of the ACM SIGPLAN \url{http://www.cs.uu.nl/~daan/hw2005/}{2005 Haskell Workshop}},
YEAR = {2005},
EDITOR = {Daan Leijen},
PAGES = {86-97},
ADDRESS = {Tallinn, Estonia},
MONTH = {September},
PUBLISHER = {ACM Press},
NOTE = {\url{http://www.cs.ru.nl/A.vanWeelden/bi-arrows/}{Source code available}},
KEYWORDS = {Haskell, Arrows, Invertible program construction, Polytypic programming},
ISBN = {1-59593-071-X},
URL = {ftp://ftp.cs.kun.nl/pub/Clean/papers/2005/alia2005-biarrowsHaskellWorkshop.pdf},
ABSTRACT = {
Invertible programming occurs in the area of data conversion where
it is required that the conversion in one direction is the inverse
of the other. For that purpose, we introduce bidirectional arrows
(bi-arrows). The bi-arrow class is an extension of Haskell's arrow
class with an extra combinator that changes the direction of
computation. The advantage of the use of bi-arrows for invertible
programming is the preservation of invertibility properties using
the bi-arrow combinators. Programming with bi-arrows in a polytypic
or generic way exploits this the most. Besides bidirectional
polytypic examples, including invertible serialization, we give the
definition of a monadic bi-arrow transformer, which we use to
construct a bidirectional parser/pretty printer.}
}
@INPROCEEDINGS{WeeldenTR05,
AUTHOR = {Arjen van Weelden and Sjaak Smetsers and Rinus Plasmeijer},
TITLE = {A Generic Approach to Syntax Tree Operations (Draft)},
BOOKTITLE = {Proceedings Implementation and Application of Functional Languages,
17th International Workshop, \url{http://www.cs.tcd.ie/ifl05/}{IFL 2005}},
YEAR = {2005},
EDITOR = {Andrew Butterfield},
NOTE = {Technical Report TCD-CS-2005-60. Preliminary version},
ADDRESS = {Dublin, Ireland},
MONTH = {September},
ORGANIZATION = {Department of Computer Science, Trinity College, University of Dublin},
ABSTRACT = {
Generic/polytypic functional programming enables the compiler to
generate most of the code. This style of programming works
especially well for the generic textbook examples, but it generally
performs poorly for bigger programs. This paper uses generic
programming to derive a parser using a types-as-grammar approach,
circumventing the need for an external parser generator and allowing
the programmer to specify everything in the language of his choice.
We show just how much we can recover from the loss of performance
using an existing optimizer on several parser monads. The
types-as-grammar approach yields a rich (non-abstract) syntax tree,
and we explore the usability of generic programming for other syntax
tree operations in a (functional) compiler, such as type inference,
scope checking, and syntax transformations.}
}
@INPROCEEDINGS{alia05:imprfusgen,
AUTHOR = {Artem Alimarine and Sjaak Smetsers},
EDITOR = {Manuel Hermenegildo and Daniel Cabeza},
MONTH = JAN,
BOOKTITLE = {Proceedings of Seventh International Symposium on Practical Aspects of Declarative Languages},
TITLE = {Improved Fusion for Optimizing Generics},
YEAR = 2005,
ORGANIZATION = {Long Beach, CA, USA},
PUBLISHER = {Springer},
SERIES = {LNCS},
NUMBER = {3350},
PAGES = {203 -- 218},
URL = {ftp://ftp.cs.kun.nl/pub/Clean/papers/2005/alia2005-ImprovedFusion.ps.gz},
ABSTRACT = {Generic programming is accepted by the functional programming
community as a valuable tool for program development. Several
functional languages have adopted the generic scheme of type-indexed
values. This scheme works by specialization of a generic function to
a concrete type. However, the generated code is extremely
inefficient compared to its hand-written counterpart. The
performance penalty is so big that the practical usefulness of
generic programming is compromised. In this paper we present an
optimization algorithm that is able to completely eliminate the
overhead introduced by the specialization scheme for a large class
of generic functions. The presented technique is based on
consumer--producer elimination as exploited by fusion, a standard
general purpose optimization method. We show that our algorithm is
able to optimize many practical examples of generic functions.
Keywords: program transformation, fusion, generic/polytypic
programming.}
}
@INPROCEEDINGS{alia04:optgenfun,
AUTHOR = {Artem Alimarine and Sjaak Smetsers},
EDITOR = {Dexter Kozen},
MONTH = JUL,
BOOKTITLE = {The 7th International Conference, Mathematics of Program Construction},
TITLE = {Optimizing Generic Functions},
YEAR = 2004,
ORGANIZATION = {Stirling, Scotland, UK},
PUBLISHER = {Springer},
SERIES = {LNCS},
NUMBER = {3125},
PAGES = {16 -- 31},
URL = {ftp://ftp.cs.kun.nl/pub/Clean/papers/2004/alia2004-OptimizingGenerics.pdf},
ABSTRACT = {Generic functions are defined by induction on the structural
representation of types. As a consequence, by defining just a
single generic operation, one acquires this operation over any
particular type. An instance on a specific type is generated by
interpretation of the type's structure. A direct translation leads
to extremely inefficient code that involves many conversions
between types and their structural representations. In this paper
we present an optimization technique based on compile-time
symbolic evaluation. We prove that the optimization removes the
overhead of the generated code for a considerable class of generic
functions. The proof uses typing to identify intermediate data
structures that should be eliminated. In essence, the output after
optimization is similar to hand-written code.}
}
@TECHREPORT{alia04:fusgen,
AUTHOR = {Artem Alimarine and Sjaak Smetsers},
TITLE = {Fusing Generic Functions},
INSTITUTION = {Nijmegen Institute for Computing and Information Sciences, University of Nijmegen, The Netherlands},
YEAR = {2004},
TYPE = {Technical report},
NUMBER = {NIII-R0434},
URL = {http://www.cs.ru.nl/research/reports/info/NIII-R0434.html}
}
@TECHREPORT{alia04:effgen,
AUTHOR = {Artem Alimarine and Sjaak Smetsers},
TITLE = {Efficient Generic Functional Programming},
INSTITUTION = {Nijmegen Institute for Computing and Information Sciences, University of Nijmegen, The Netherlands},
YEAR = {2004},
TYPE = {Technical report},
NUMBER = {NIII-R0425},
URL = {http://www.cs.ru.nl/research/reports/info/NIII-R0425.html}
}
@INPROCEEDINGS{arkd03:fusion,
AUTHOR = {{Arkel}, {Diederik van} and {Groningen}, {John van} and Smetsers, Sjaak},
EDITOR = {Pe\~{n}a, Ricardo and Arts, Thomas},
BOOKTITLE = {The 14th International Workshop on the Implementation of Functional Languages, IFL'02, Selected Papers},
TITLE = {Fusion in Practice},
PAGES = {51--67},
YEAR = 2003,
VOLUME = {2670},
PUBLISHER = {Springer},
SERIES = {LNCS},
URL = {ftp://ftp.cs.kun.nl/pub/Clean/papers/2003/arkd2003-FusionInPractice.pdf},
ABSTRACT = {Deforestation was introduced to eliminate intermediate data
structures used to connect separate parts of a functional program
together. Fusion is a more sophisticated technique, based on a
producer-consumer model, to eliminate intermediate data structures.
It achieves better results. In this paper we extend this
fusion algorithm by refining this model, and by adding new
transformation rules. The extended fusion algorithm is able to
deal with standard deforestation, but also with higher-order function
removal and dictionary elimination. We have implemented this
extended algorithm in the Clean 2.0 compiler.}
}
@INBOOK{bare99:uniquenessHandbook,
AUTHOR = {Erik Barendsen and Sjaak Smetsers},
TITLE = {Graph Rewriting Aspects of Functional Programming},
CHAPTER = {2},
PAGES = {63-102},
PUBLISHER = {World scientific},
YEAR = {1999},
CROSSREF = {ehrh99:handbookgraphgrammars},
URL = {http://www.wspc.com/books/compsci/4180.html}
}
@INPROCEEDINGS{bare98:strictnesstyping,
AUTHOR = {Barendsen, Erik and Smetsers, Sjaak},
TITLE = {Strictness Typing},
BOOKTITLE = {Proceedings of the 10th International Workshop on Implementation of Functional Languages, IFL 1998},
EDITOR = {Kevin Hammond and Tony Davie and Chris Hankin},
ADDRESS = {University College London, United Kingdom},
PAGES = {101--116},
YEAR = {1998},
ABSTRACT = {}
}
@INPROCEEDINGS{bare96:uniquenessTypingForFLs,
AUTHOR = {Erik Barendsen and Sjaak Smetsers},
TITLE = {Uniqueness typing for functional languages with graph rewriting semantics},
BOOKTITLE = {Mathematical Structures in Computer Science},
VOLUME = {6},
PAGES = {579-612},
YEAR = {1996},
URL = {http://www.cs.ru.nl/~clean/download/papers/1996/bare96-uniclosed.pdf},
ABSTRACT = {We present two type systems for term graph rewriting: conventional typing and
(polymorphic) uniqueness typing. The latter is introduced as a natural extension
of simple algebraic and higher-order uniqueness typing. The systems are given in
natural deduction style using an inductive syntax of graph denotations with
familiar constructs such as let and case.
The conventional system resembles traditional Curry-style typing systems in
functional programming languages. Uniqueness typing extends this with reference
count information. In both type systems, typing is preserved during evaluation,
and types can be determined effectively. Moreover, with respect to a graph
rewriting semantics, both type systems turn out to be sound.}
}
@BOOK{ehrh99:handbookgraphgrammars,
AUTHOR = {Ehrig, H. and Engels, G. and Kreowski, {H.-J.} and Rozenberg, G.},
TITLE = {Handbook of Graph Grammars and Computing by Graph Transformation},
PUBLISHER = {World Scientific},
YEAR = {1999}
}
This file has been generated by bibtex2html 1.74