[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 |

[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 Peña 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. |

[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*