[1] Martijn Stegeman, Erik Barendsen, and Sjaak Smetsers. Towards an empirically validated model for assessment of code quality. In Proceedings of the 14th Koli Calling International Conference on Computing Education Research, Koli Calling '14, pages 99-108, New York, NY, USA, 2014. ACM.
[ bib ]
Keywords: assessment, code quality, empirical validation, feedback, programming education, rubrics
[2] DanielJ. Bernstein, Bernard van Gastel, Wesley Janssen, Tanja Lange, Peter Schwabe, and Sjaak Smetsers. Tweetnacl: A crypto library in 100 tweets. In Diego F. Aranha and Alfred Menezes, editors, Progress in Cryptology - LATINCRYPT 2014, volume 8895 of Lecture Notes in Computer Science, pages 64-83. Springer International Publishing, 2015.
[ bib | http ]
Keywords: Trusted code base; Source-code size; Auditability; Software implementation; Timing-attack protection; NaCl; Twitter
[3] Ken Madlener, Sjaak Smetsers, and Marko van Eekelen. Modular bialgebraic semantics and algebraic laws. In Proceedings of SBLP'13, volume 8129, pages 46-60. LNCS, 2013.
[ bib ]
[4] Ken Madlener and Sjaak Smetsers. GSOS formalized in Coq. In Proceedings of TASE'13, pages 199-206. IEEE, 2013.
[ bib ]
[5] Sjaak Smetsers and Erik Barendsen. Verifying functional formalizations - a type-theoretical case study in pvs. In Peter Achten and Pieter W. M. Koopman, editors, The Beauty of Functional Code, volume 8106, pages 47-59, 2013.
[ bib ]
[6] Rody Kersten, Bernard van Gastel, Manu Drijvers, Sjaak Smetsers, and Marko van Eekelen. Using model-checking to reveal a vulnerability of tamper-evident pairing. In G. Brat, N. Rungta, and A. Venet, editors, Proceedings of the 5th NASA Formal Methods Symposium., number 7871 in Lecture Notes in Computer Science, pages 63-77. Springer, May 2013.
[ bib ]
[7] Ken Madlener, Sjaak Smetsers, and Marko van Eekelen. Modular bialgebraic semantics and algebraic laws. Technical Report ICIS-R13008, Radboud University Nijmegen, July 2013.
[ bib ]
[8] Sjaak Smetsers and Marko van Eekelen. Higher-order strictness typing. In Hans-Wolfgang Loidl and Ricardo Peña, editors, Trends in Functional Programming, volume 7829 of Lecture Notes in Computer Science, pages 85-100. Springer Berlin Heidelberg, 2013.
[ bib | http ]
[9] Leonard Lensink, Sjaak Smetsers, and Marko C. J. D. van Eekelen. A proof framework for concurrent programs. In Derrick et al. [10], pages 174-190.
[ bib ]
[10] John Derrick, Stefania Gnesi, Diego Latella, and Helen Treharne, editors. Integrated Formal Methods - 9th International Conference, IFM 2012, Pisa, Italy, June 18-21, 2012. Proceedings, volume 7321 of Lecture Notes in Computer Science. Springer, 2012.
[ bib ]
[11] Leonard Lensink, Sjaak Smetsers, and Marko C. J. D. van Eekelen. Generating verifiable java code from verified pvs specifications. In Goodloe and Person [12], pages 310-325.
[ bib ]
[12] Alwyn Goodloe and Suzette Person, editors. NASA Formal Methods - 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings, volume 7226 of Lecture Notes in Computer Science. Springer, 2012.
[ bib ]
[13] Ken Madlener, Sjaak Smetsers, and Marko van Eekelen. Formal component-based semantics. In Michel A. Reniers and Pawel Sobocinski, editors, Proceedings of the 8th Workshop on Structural Operational Semantics (SOS'11), volume 62 of Electronic Proceedings in Theoretical Computer Science, pages 17-29, 2011.
[ bib ]
[14] Ken Madlener, Sjaak Smetsers, and Marko van Eekelen. A formal verification study on the Rotterdam storm surge barrier. In Jin Song Dong and Huibiao Zhu, editors, Proceedings of the 12th International Conference on Formal Engineering Methods (IFCEM'10), volume 6447 of LNCS, pages 287-302. Springer, 2010.
[ bib ]
[15] Leonard Lensink, Sjaak Smetsers, and Marko C. J. D. van Eekelen. Machine checked formal proof of a scheduling protocol for smartcard personalization. In Leue and Merino [16], pages 115-132.
[ bib ]
[16] Stefan Leue and Pedro Merino, editors. Formal Methods for Industrial Critical Systems, 12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers, volume 4916 of Lecture Notes in Computer Science. Springer, 2008.
[ bib ]
[17] Sjaak Smetsers. The syntactic continuity property: A computer verified proof. In Sun-Yuan Hsieh Jixin Ma Zoran Majkic and Khalid S HusainEditors Ibrahiem M M El Emary, editors, International Conference on Theoretical and Mathematical Foundations of Computer Science (TMFCS10), pages 135-142. ISRST, 2010.
[ bib ]
[18] Erik Schierboom, Alejandro Tamalet, Hendrik Tews, Marko van Eekelen, and Sjaak Smetsers. Preemption abstraction: A lightweight approach to modelling concurrency. In Formal Methods for Industrial Critical Systems (FMICS 2009), volume 5825, pages 149-164, 2009.
[ bib ]
[19] Sjaak Smetsers and Marko Eekelen, van. Laquso: Using formal methods for analysis, verification and improvement of safety critical software. Quarterly Magazine of the European Research Consortium for Informatics and Mathematics. Special Theme Safety-Critical Software, 75:38-39, October 2008.
[ bib ]
[20] Sjaak Smetsers, Arjen van Weelden, and Rinus Plasmeijer. Efficient and type-safe generic data storage. Electron. Notes Theor. Comput. Sci., 238(2):59-70, June 2009.
[ bib ]
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.
Keywords: Polytypic/generic programming, data storage/sequentialization, functional programming, type inference
[21] Sjaak Smetsers and Erik Barendsen. Formalizing Type Theory in PVS: a case study. Technical Report ICIS-R08022, Radboud University Nijmegen, December 2008.
[ bib ]
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.
[22] Rinus Plasmeijer, Sjaak Smetsers, and Arjen van Weelden. Interactive Combining of Typed Object Code. Technical Report ICIS-R08019, Radboud University Nijmegen, November 2008.
[ bib ]
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 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.
[23] Erik Barendsen and Sjaak Smetsers. Strictness analysis via resource typing. In Reflections on Type Theory, Lambda Calculus, and the Mind, pages 29-40, Nijmegen, Netherlands, December 2007.
[ bib ]
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.
[24] Leonard Lensink, Sjaak Smetsers, and Marko van Eekelen. Machine checked formal proof of a scheduling protocol for smartcard personalization. In 12th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2007, Lecture Notes in Computer Science, Berlin, Germany, July 2007. Springer.
[ bib ]
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.
[25] Bart Jacobs, Sjaak Smetsers, and Ronny Wichers Schreur. Code-carrying theories. Formal Asp. Comput., 19(2):191-203, 2007.
[ bib ]
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.
[26] Sjaak Smetsers and Arjen van Weelden. Bracket-abstraction preserves typability: A formal proof of Diller-algorithm-C in PVS. UNIF 2006, August 2006.
[ bib ]
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.
[27] Arjen van Weelden, Sjaak Smetsers, and Rinus Plasmeijer. Polytypic syntax tree operations. In Implementation and Application of Functional Languages, 17th International Workshop, IFL 2005, Revised Selected Papers, Lecture Notes in Computer Science, Dublin, Ireland, September 2005. Springer.
[ bib ]
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.
[28] Artem Alimarine, Sjaak Smetsers, Arjen van Weelden, Marko van Eekelen, and Rinus Plasmeijer. There and back again: Arrows for invertible programming. In Daan Leijen, editor, Proceedings of the ACM SIGPLAN http://www.cs.uu.nl/~daan/hw2005/2005 Haskell Workshop, pages 86-97, Tallinn, Estonia, September 2005. ACM Press. http://www.cs.ru.nl/A.vanWeelden/bi-arrows/Source code available.
[ bib | .pdf ]
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.
Keywords: Haskell, Arrows, Invertible program construction, Polytypic programming
[29] Arjen van Weelden, Sjaak Smetsers, and Rinus Plasmeijer. A generic approach to syntax tree operations (draft). In Andrew Butterfield, editor, Proceedings Implementation and Application of Functional Languages, 17th International Workshop, http://www.cs.tcd.ie/ifl05/IFL 2005, Dublin, Ireland, September 2005. Department of Computer Science, Trinity College, University of Dublin. Technical Report TCD-CS-2005-60. Preliminary version.
[ bib ]
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.
[30] Artem Alimarine and Sjaak Smetsers. Improved fusion for optimizing generics. In Manuel Hermenegildo and Daniel Cabeza, editors, Proceedings of Seventh International Symposium on Practical Aspects of Declarative Languages, number 3350 in LNCS, pages 203 - 218. Long Beach, CA, USA, Springer, January 2005.
[ bib | .ps.gz ]
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.
[31] Artem Alimarine and Sjaak Smetsers. Optimizing generic functions. In Dexter Kozen, editor, The 7th International Conference, Mathematics of Program Construction, number 3125 in LNCS, pages 16 - 31. Stirling, Scotland, UK, Springer, July 2004.
[ bib | .pdf ]
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.
[32] Artem Alimarine and Sjaak Smetsers. Fusing generic functions. Technical report NIII-R0434, Nijmegen Institute for Computing and Information Sciences, University of Nijmegen, The Netherlands, 2004.
[ bib | .html ]
[33] Artem Alimarine and Sjaak Smetsers. Efficient generic functional programming. Technical report NIII-R0425, Nijmegen Institute for Computing and Information Sciences, University of Nijmegen, The Netherlands, 2004.
[ bib | .html ]
[34] Diederik van Arkel, John van Groningen, and Sjaak Smetsers. Fusion in practice. In Ricardo Pea and Thomas Arts, editors, The 14th International Workshop on the Implementation of Functional Languages, IFL'02, Selected Papers, volume 2670 of LNCS, pages 51-67. Springer, 2003.
[ bib | .pdf ]
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.
[35] Erik Barendsen and Sjaak Smetsers. Graph Rewriting Aspects of Functional Programming, chapter 2, pages 63-102. In [38], 1999.
[ bib | .html ]
[36] Erik Barendsen and Sjaak Smetsers. Strictness typing. In Kevin Hammond, Tony Davie, and Chris Hankin, editors, Proceedings of the 10th International Workshop on Implementation of Functional Languages, IFL 1998, pages 101-116, University College London, United Kingdom, 1998.
[ bib ]
[37] Erik Barendsen and Sjaak Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. In Mathematical Structures in Computer Science, volume 6, pages 579-612, 1996.
[ bib | .pdf ]
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.

[38] H. Ehrig, G. Engels, H.-J. Kreowski, and G. Rozenberg. Handbook of Graph Grammars and Computing by Graph Transformation. World Scientific, 1999.
[ bib ]

This file has been generated by bibtex2html 1.74