/
types.bib
6995 lines (5663 loc) · 268 KB
/
types.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
% types.bib -- Bibliography for work related to types in programming languages
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Immutability
%%%
@InProceedings{PoratBKM2000,
author = "Sara Porat and Marina Biberstein and Larry Koved and
Bilba Mendelson",
title = "Automatic detection of immutable fields in {Java}",
crossref = "CASCON2000",
NEEDpages = "*",
abstract =
"This paper introduces techniques to detect mutability of fields and classes
in Java. A variable is considered to be mutable if a new value is stored
into it, as well as if any of its reachable variables is mutable. We
present a static flow-sensitive analysis algorithm which can be applied to
any Java component. The analysis classifies fields and classes as either
mutable or immutable. In order to facilitate open-world analysis, the
algorithm identifies situations that expose variables to potential
modification by code outside the component, as well as situations where
variables are modified by the analyzed code. We also present an
implementation of the analysis which focuses on detecting mutability of
class variables, so as to avoid isolation problems. The implementation
incorporates intra- and inter-procedural data-flow analyses and is shown to
be highly scalable. Experimental results demonstrate the effectiveness of
the algorithms."
}
@InProceedings{BibersteinGP01,
author = "Marina Biberstein and Joseph Gil and Sara Porat",
title = "Sealing, encapsulation, and mutability",
crossref = "ECOOP2001",
pages = "28--52",
}
@InProceedings{SkoglundW2001,
author = "Mats Skoglund and Tobias Wrigstad",
title = "A mode system for read-only references in {Java}",
crossref = "FTFJP2001",
NEEDpages = "*",
}
@TechReport{MuellerPoetzsch-Heffter01a,
author = { M{\"u}ller, P. and Poetzsch-Heffter, A. },
title = { Universes: A Type System
for Alias and Dependency Control },
institution = { Fernuniversit{\"a}t Hagen },
year = 2001,
number = 279,
note = { }
}
@Article{DietlM2005,
author = "Werner Dietl and Peter M{\"u}ller",
authorASCII = "Peter Muller / Peter Mueller",
title = "Universes: Lightweight ownership for {JML}",
journal = JOT,
year = 2005,
volume = 4,
number = 8,
pages = "5--32",
month = oct
}
@InProceedings{DietlDM2007,
author = "Werner Dietl and Sophia Drossopoulou and Peter M{\"u}ller",
authorASCII = "Peter Muller",
title = "{G}eneric {U}niverse {T}ypes",
titleASCII = "Generic Universe Types",
crossref = "ECOOP2007",
pages = "28--53",
abstract =
"Ownership is a powerful concept to structure the object store and to
control aliasing and modifications of objects. This paper presents an
ownership type system for a Java-like programming language with generic
types. Like our earlier Universe type system, Generic Universe Types
enforce the owner-as-modifier discipline. This discipline does not restrict
aliasing, but requires modifications of an object to be initiated by its
owner. This allows owner objects to control state changes of owned objects,
for instance, to maintain invariants. Generic Universe Types require a
small annotation overhead and provide strong static guarantees. They are
the first type system that combines the owner-as-modifier discipline with
type genericity.",
}
@Article{KnieselT2001,
author = "G{\"u}nter Kniesel and Dirk Theisen",
title = "{JAC} --- Access right based encapsulation for {Java}",
journal = j-spe,
year = 2001,
volume = 31,
number = 6,
pages = "555--576"
}
@InProceedings{PechtchanskiS2002,
author = "Igor Pechtchanski and Vivek Sarkar",
title = "Immutability specification and its applications",
crossref = "JavaGrande2002",
pages = "202--211",
abstract =
"A location is said to be immutable if its value and the values of selected
locations reachable from it are guaranteed to remain unchanged during a
specified time interval. We introduce a framework for immutability
specification, and discuss its application to code optimization. Compared
to a final declaration, an immutability assertion in our framework can
express a richer set of immutability properties along three dimensions ---
lifetime, reachability and context. We present a framework for processing
and verifying immutability annotations in Java, as well as extending
optimizations so as to exploit immutability information. Preliminary
experimental results show that a significant number (82\%) of read accesses
could potentially be classified as immutable in our framework. Further, use
of immutability information yields substantial reductions (33\% to 99\%) in
the number of dynamic read accesses, and also measurable speedups in the
range of 5\% to 10\% for certain benchmark programs."
}
@InProceedings{BoylandNR2001,
author = "John Boyland and James Noble and William Retert",
title = "Capabilities for sharing:
A generalisation of uniqueness and read-only",
crossref = "ECOOP2001",
pages = "2--27",
abstract =
"Many languages and language extensions include annotations on pointer
variables such as ``read-only,'' ``unique,'' and ``borrowed''; many more
annotations have been proposed but not implemented. Unfortunately, all
these annotations are described individually and formalised independently -
assuming they are formalised at all. In this paper, we show how these
annotations can be subsumed into a general capability system for
pointers. This system separates mechanism (defining the semantics of
sharing and exclusion) from policy (defining the invariants that are
intended to be preserved). The capability system has a well-defined
semantics which can be used as a reference for the correctness of various
extended type systems using annotations. Furthermore, it supports research
in new less-restrictive type systems that permit a wider range of idioms to
be statically checked."
}
@InProceedings{Boyland2005,
author = "John Boyland",
title = "Why we should not add \texttt{readonly} to {Java} (yet)",
crossref = "FTFJP2005",
NEEDpages = "",
abstract =
"In this paper, I examine some of reasons that ``readonly'' style
qualifiers have been proposed for Java, and also the principles behind the
rules for these new qualifiers. I find that there is a mismatch between
some of the motivating problems and the proposed solutions. Thus I urge
Java designers to proceed with caution when adopting a solution to these
sets of problems.",
}
@Misc{JSR163,
author = "Robert Field",
title = "{JSR} 163: {Java} Platform Profiling Architecture",
howpublished = "\url{https://jcp.org/en/jsr/detail?id=163}",
month = sep # "~30,",
year = 2004,
}
@Misc{JSR175,
author = "Joshua Bloch",
title = "{JSR} 175: A Metadata Facility for the {Java} Programming Language",
howpublished = "\url{https://jcp.org/en/jsr/detail?id=175}",
month = sep # "~30,",
year = 2004,
}
@Misc{JSR175-PFD2,
author = "Joshua Bloch",
title = "{JSR175}: A Program Annotation Facility for the {Java} Programming Language: Proposed Final Draft 2",
howpublished = "\url{https://jcp.org/en/jsr/detail?id=175}",
month = aug # "~12,",
year = 2004,
}
@Misc{JSR198,
author = "Jose Cronembold",
title = "{JSR} 198: A Standard Extension {API} for {Integrated} {Development} {Environments}",
howpublished = "\url{https://jcp.org/en/jsr/detail?id=198}",
month = may # "~8,",
year = 2006,
}
@Misc{JSR199,
author = "Peter von der Ahe",
title = "{JSR} 199: {Java} Compiler {API}",
howpublished = "\url{https://jcp.org/en/jsr/detail?id=199}",
month = dec # "~11,",
year = 2006,
}
@Misc{JSR250,
author = "Rajiv Mordani",
title = "{JSR} 250: Common Annotations for the {Java} Platform",
howpublished = "\url{https://jcp.org/en/jsr/detail?id=250}",
month = may # "~11,",
year = 2006,
}
@Misc{JSR269,
author = "Joe Darcy",
title = "{JSR} 269: Pluggable Annotation Processing {API}",
howpublished = "\url{https://jcp.org/en/jsr/detail?id=269}",
month = may # "~17,",
year = 2006,
note = "Public review version",
}
@Misc{JSR305,
author = "William Pugh",
title = "{JSR} 305: Annotations for Software Defect Detection",
howpublished = "\url{https://jcp.org/en/jsr/detail?id=305}",
month = aug # "~29,",
year = 2006,
note = "JSR Review Ballot version",
}
@InProceedings{HaackPSS2007,
author = "Christian Haack and Erik Poll and Jan Sch{\"a}fer and Aleksy Schubert",
title = "Immutable objects for a {Java}-like language",
crossref = "ESOP2007",
pages = "347--362",
}
@InProceedings{HaackP2009,
author = "Haack, Christian and Poll, Erik",
title = "Type-Based Object Immutability with Flexible Initialization",
crossref = "ECOOP2009",
pages = "520--545",
abstract =
"We present a type system for checking object immutability, read-only
references, and class immutability in an open or closed world. To allow
object initialization outside object constructors (which is often needed in
practice), immutable objects are initialized in lexically scoped
regions. The system is simple and direct; its only type qualifiers specify
immutability properties. No auxiliary annotations, e.g., ownership types,
are needed, yet good support for deep immutability is provided. To express
object confinement, as required for class immutability in an open world, we
use qualifier polymorphism. The system has two versions: one with explicit
specification commands that delimit the object initialization phase, and
one where such commands are implicit and inferred. In the latter version,
all annotations are compatible with Java's extended annotation syntax, as
proposed in JSR 308.",
}
@MastersThesis{Noack2010,
author = "Gunther Noack",
title = "{TIFI}+: A Type Checker for Object Immutability with Flexible Initialization",
school = "University of Kaiserslautern",
year = 2010,
type = "Diploma thesis",
month = mar,
}
@InProceedings{CoblenzNAMS2017,
author = "Coblenz, Michael and Nelson, Whitney and Aldrich, Jonathan and Myers, Brad and Sunshine, Joshua",
title = "Glacier: Transitive class immutability for {Java}",
crossref = "ICSE2017",
pages = "496--506",
}
@PhdThesis{Coblenz2020,
author = "Michael Coblenz",
title = "User-Centered Design of Principled Programming Languages",
school = "Carnegie Mellon University",
year = 2020,
month = "aug",
note = "TR CMU-CS-20-127",
}
@InProceedings{Milanova2018,
author = "Ana Milanova",
title = "Definite reference mutability",
crossref = "ECOOP2018",
pages = "25:1--25:30",
}
@InProceedings{CoblenzSAMWS2016,
author = "Coblenz, Michael and Sunshine, Joshua and Aldrich, Jonathan and Myers, Brad and Weber, Sam and Shull, Forrest",
title = "Exploring Language Support for Immutability",
crossref = "ICSE2016",
pages = "736-747",
}
@MastersThesis{Sun2021,
author = "Lian Sun",
title = "An Immutability Type System for Classes and Objects: Improvements, Experiments, and Comparisons",
school = UWaterlooECE,
year = 2021,
address = UWaterlooaddr,
month = apr,
}
%%%
%%% Interning (aka canonicalization, hash-consing)
%%%
@Article{Ershov58,
author = "A. P. Ershov",
title = "On programming of arithmetic operations",
journal = CACM,
year = 1958,
volume = 1,
number = 8,
pages = "3--6",
month = aug,
}
@Book{Allen78,
author = "John R. Allen",
title = "Anatomy of LISP",
publisher = "McGraw-Hill",
year = 1978,
address = "New York",
}
@TechReport{Goto74,
author = "E. Goto",
title = "Monocopy and associative algorithms in an extended {Lisp}",
institution = "Information Science Laboratory, University of Tokyo",
year = 1974,
number = "74-03",
address = "Tokyo, Japan",
month = may,
}
@InProceedings{VaziriTFD2007,
author = "Mandana Vaziri and Frank Tip and Stephen Fink and Julian Dolby",
title = "Declarative object identity using relation types",
crossref = "ECOOP2007",
pages = "54--78",
}
@InProceedings{MarinovO2003,
author = "Darko Marinov and Robert O'Callahan",
title = "Object equality profiling",
crossref = "OOPSLA2003",
pages = "313--325",
abstract =
"We present \emph{Object Equality Profiling} (OEP), a new technique for
helping programmers discover optimization opportunities in programs. OEP
discovers opportunities for replacing a set of equivalent object instances
with a single representative object. Such a set represents an opportunity for
automatically or manually applying optimizations such as hash consing, heap
compression, lazy allocation, object caching, invariant hoisting, and
more. To evaluate OEP, we implemented a tool to help programmers reduce the
memory usage of Java programs. Our tool performs a dynamic analysis that
records all the objects created during a particular program run. The tool
partitions the objects into equivalence classes, and uses collected timing
information to determine when elements of an equivalence class could have
been safely collapsed into a single representative object without affecting
the behavior of that program run. We report the results of applying this
tool to benchmarks, including two widely used Web application servers. Many
benchmarks exhibit significant amounts of object equivalence, and in most
benchmarks our profiler identifies optimization opportunities clustered
around a small number of allocation sites. We present a case study of using
our profiler to find simple manual optimizations that reduce the average
space used by live objects in two SpecJVM benchmarks by 47\% and 38\%
respectively.",
}
@InProceedings{ZendraC99,
author = "Olivier Zendra and Dominique Colnet",
title = "Towards safer aliasing with the {Eiffel} language",
crossref = "IWAOOS99",
pages = "153--154",
}
@InProceedings{120750,
author = {Richard J. Fateman},
title = {Canonical representations in Lisp and applications to computer algebra systems},
booktitle = {ISSAC '91: Proceedings of the 1991 international symposium on Symbolic and algebraic computation},
year = {1991},
isbn = {0-89791-437-6},
pages = {360--369},
address = {Bonn, West Germany},
doi = {https://doi.acm.org/10.1145/120694.120750},
}
@article{231195,
author = {Richard J. Fateman and Mark Hayden},
title = {Speeding up Lisp-based symbolic mathematics},
journal = {SIGSAM Bull.},
volume = {30},
number = {1},
year = {1996},
issn = {0163-5824},
pages = {25--30},
doi = {https://doi.acm.org/10.1145/231191.231195},
}
@InProceedings{FilliatreC2006,
author = "Jean-Christophe Filli\^{a}tre and Sylvain Conchon",
authorASCII = "Jean-Christophe Filliatre and Sylvain Conchon",
title = "Type-safe modular hash-consing",
crossref = "ML2006",
pages = "12--19",
}
%% These last few citations are unrelated to interning, but seemed to be at
%% first glance.
@article{359667,
author = {Jay M. Spitzen and Karl N. Levitt and Lawrence Robinson},
title = {An example of hierarchical design and proof},
journal = CACM,
volume = {21},
month = dec,
number = {12},
year = {1978},
issn = {0001-0782},
pages = {1064--1075},
doi = {https://doi.acm.org/10.1145/359657.359667},
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Type qualifiers in general (not immutability)
%%%
@InProceedings{FosterFFA99,
author = "Jeffrey S. Foster and Manuel F{\"{a}}hndrich and
Alexander Aiken",
title = "A theory of type qualifiers",
crossref = "PLDI99",
pages = "192--203",
doi = {10.1145/301618.301665},
}
@Article{FosterJKA2006,
author = "Jeffrey S. Foster and Robert Johnson and John Kodumal and Alex Aiken ",
title = "Flow-insensitive type qualifiers",
journal = TOPLAS,
year = 2006,
volume = 28,
number = 6,
pages = "1035--1087",
month = nov,
abstract =
"We describe flow-insensitive type qualifiers, a lightweight, practical
mechanism for specifying and checking properties not captured by
traditional type systems. We present a framework for adding new,
user-specified type qualifiers to programming languages with static type
systems, such as C and Java. In our system, programmers add a few type
qualifier annotations to their program, and automatic type qualifier
inference determines the remaining qualifiers and checks the annotations
for consistency. We describe a tool CQual for adding type qualifiers to the
C programming language. Our tool CQual includes a visualization component
for displaying browsable inference results to the programmer. Finally, we
present several experiments using our tool, including inferring const
qualifiers, finding security vulnerabilities in several popular C programs,
and checking initialization data usage in the Linux kernel. Our results
suggest that inference and visualization make type qualifiers lightweight,
that type qualifier inference scales to large programs, and that type
qualifiers are applicable to a wide variety of problems.",
}
@InProceedings{foster:PLDI02,
author = {Jeffrey S. Foster and Tachio Terauchi and Alex Aiken},
title = "Flow-sensitive type qualifiers",
crossref = "PLDI2002",
pages = {1--12},
}
@Manual{ElsmanFA99,
title = "Carillon --- A System to Find {Y2K} Problems in {C} Programs",
author = "Martin Elsman and Jeffrey S. Foster and Alexander Aiken",
month = jul # "~30,",
year = 1999,
abstract =
"Carillon is a simple, fast, and effective type-based system for finding Y2K
errors in C programs. Carillon extends the standard C type system with a
user-defined set of date-related type qualifiers. The user annotates
date-related functions with the appropriate qualifiers, and Carillon checks
the program for Y2K errors.
\par
Carillon displays the results of the Y2K analysis in an interactive Emacs
buffer. Program variables are colored according to the kind of Y2K
information they may contain, and the user can click on program variables
to see the exact Y2K type inferred by the analysis.
\par
The system has been used successfully to verify Y2K readiness of programs
and to locate Y2K errors.",
URL = "www.cs.berkeley.edu/Research/Aiken/carillon/",
}
@InProceedings{GreenfieldboyceF2007,
author = "David Greenfieldboyce and Jeffrey S. Foster",
title = "Type qualifier inference for {Java}",
crossref = "OOPSLA2007",
pages = "321--336",
abstract =
"Java's type system provides programmers with strong guarantees of type and
memory safety, but there are many important properties not captured by
standard Java types. We describe JQual, a tool that adds user-defined type
qualifiers to Java, allowing programmers to quickly and easily incorporate
extra lightweight, application-specific type checking into their
programs. JQual provides type qualifier inference, so that programmers need
only add a few key qualifier annotations to their program, and then JQual
infers any remaining qualifiers and checks their consistency. We explore
two applications of JQual. First, we introduce opaque and enum qualifiers
to track C pointers and enumerations that flow through Java code via the
JNI. In our benchmarks we found that these C values are treated correctly,
but there are some places where a client could potentially violate
safety. Second, we introduce a readonly qualifier for annotating references
that cannot be used to modify the objects they refer to. We found that
JQual is able to automatically infer readonly in many places on method
signatures. These results suggest that type qualifiers and type qualifier
inference are a useful addition to Java.",
}
@Misc{GreenfieldboyceF2005,
author = "David Greenfieldboyce and Jeffrey S. Foster",
title = "Type qualifiers for {Java}",
howpublished = "\url{http://www.cs.umd.edu/Grad/scholarlypapers/papers/greenfiledboyce.pdf}",
month = aug # "~8,",
year = 2005,
supersededby = "GreenfieldboyceF2007",
}
@InProceedings{ChinMM2005,
author = "Brian Chin and Shane Markstrum and Todd Millstein",
title = "Semantic type qualifiers",
crossref = "PLDI2005",
pages = "85--95",
abstract =
"We present a new approach for supporting user-defined type refinements,
which augment existing types to specify and check additional invariants of
interest to programmers. We provide an expressive language in which users
define new refinements and associated type rules. These rules are
automatically incorporated by an \emph{extensible typechecker} during
static typechecking of programs. Separately, a \emph{soundness checker}
automatically proves that each refinement's type rules ensure the intended
invariant, for all possible programs. We have formalized our approach and
have instantiated it as a framework for adding new type qualifiers to C
programs. We have used this framework to define and automatically prove
sound a host of type qualifiers of different sorts, including \texttt{pos}
and \texttt{neg} for integers, \texttt{tainted} and \texttt{untainted} for
strings, and \texttt{nonnull} and \texttt{unique} for pointers, and we have
applied our qualifiers to ensure important invariants on open-source C
programs.",
}
@InProceedings{ChinMMP2006,
author = "Brian Chin and Shane Markstrum and Todd Millstein and Jens Palsberg",
title = "Inference of user-defined type qualifiers and qualifier rules",
crossref = "ESOP2006",
pages = "264--278",
}
@InProceedings{MandelbaumWH2003,
author = "Yitzhak Mandelbaum and David Walker and Robert Harper",
title = "An effective theory of type refinements",
crossref = "ICFP2003",
pages = "213--225",
abstract =
"We develop an explicit two level system that allows programmers to reason
about the behavior of effectful programs. The first level is an ordinary
ML-style type system, which confers standard properties on program
behavior. The second level is a conservative extension of the first that
uses a logic of type refinements to check more precise properties of
program behavior. Our logic is a fragment of intuitionistic linear logic,
which gives programmers the ability to reason locally about changes of
program state. We provide a generic resource semantics for our logic as
well as a sound, decidable, syntactic refinement-checking system. We also
prove that refinements give rise to an optimization principle for
programs. Finally, we illustrate the power of our system through a number
of examples.",
}
@InProceedings{deline04typestates,
author = "Robert DeLine and Manuel F{\"a}hndrich",
title = "Typestates for objects",
crossref = "ECOOP2004",
pages = "465--490",
}
@InProceedings{DeLineF2001,
author = "Robert DeLine and Manuel F{\"a}hndrich",
title = "Enforcing high-level protocols in low-level software",
crossref = "PLDI2001",
pages = "59--69",
}
@InProceedings{ShankarTFW2001,
author = "Umesh Shankar and Kunal Talwar and Jeffrey S. Foster and David Wagner",
title = "Detecting format string vulnerabilities with type qualifiers",
crossref = "USENIXSec2001",
NEEDpages = "*",
}
@InProceedings{VolpanoS97,
author = "Dennis M. Volpano and Geoffrey Smith",
title = "A type-based approach to program security",
crossref = "TAPSOFT97",
pages = "607--621",
}
@InProceedings{PalsbergO95,
author = "Jens Palsberg and Peter {\O}rb{\ae}k",
authorASCII = "Peter Orbaek",
title = "Trust in the $\lambda$-calculus",
crossref = "SAS95",
pages = "314--329",
}
@InProceedings{PratikakisSH2004,
author = "Polyvios Pratikakis and Jaime Spacco and Michael Hicks",
title = "Transparent proxies for {Java} futures",
crossref = "OOPSLA2004",
pages = "206--223",
}
@InProceedings{JohnsonW2004,
author = "Rob Johnson and David Wagner",
title = "Finding user/kernel pointer bugs with type inference",
crossref = "USENIXSec2004",
pages = "119--134",
}
@Article{YelickSPMLKHGGCA1998,
author = "Kathy Yelick and Luigi Semenzato and Geoff Pike and Carleton Miyamoto and Ben Liblit and Arvind Krishnamurthy and Paul Hilfinger and Susan Graham and David Gay and Phil Colella and Alex Aiken",
title = "Titanium: A high-performance {Java} dialect",
journal = "Concurrency: Practice and Experience",
year = 1998,
volume = 10,
number = "11--13",
pages = "825--836",
month = sep # "--" # nov,
abstract =
"Titanium is a language and system for high-performance parallel
scientific computing. Titanium uses Java as its base, thereby leveraging
the advantages of that language and allowing us to focus attention on
parallel computing issues. The main additions to Java are immutable
classes, multidimensional arrays, an explicitly parallel SPMD model of
computation with a global address space, and zone-based memory
management. We discuss these features and our design approach, and
report progress on the development of Titanium, including our current
driving application: a three-dimensional adaptive mesh refinement
parallel Poisson solver.",
}
%%%
%%% Non-null (nonnull) types and nullness/nullity analysis
%%%
@InProceedings{FahndrichL2003:OOPSLA,
author = "Manuel F{\"a}hndrich and K. Rustan M. Leino",
authorASCII = "Manuel Fahndrich",
title = "Declaring and checking non-null types in an
object-oriented language",
crossref = "OOPSLA2003",
pages = "302--312",
abstract =
"Distinguishing non-null references from possibly-null references at the
type level can detect null-related errors in object-oriented programs at
compile-time. This paper gives a proposal for retrofitting a language such
as C\# or Java with non-null types. It addresses the central complications
that arise in constructors, where declared non-null fields may not yet have
been initialized, but the partially constructed object is already
accessible. The paper reports experience with an implementation for
annotating and checking null-related properties in C\# programs.",
}
@InProceedings{FahndrichLeino03:IWACO,
author = {Manuel F{\"a}hndrich and K. Rustan M. Leino},
authorASCII = {Manuel Fahndrich and K. Rustan M. Leino},
title = {Heap Monotonic Typestates},
crossref = "IWACO2003",
pages = "58-72",
abstract =
"The paper defines the class of heap monotonic typestates. The
monotonicity of such typestates enables sound checking algorithms
without the need for non-aliasing regimes of pointers. The basic idea is
that data structures evolve over time in a manner that only makes their
representation invariants grow stronger, never weaker. This assumption
guarantees that existing object references with particular typestates
remain valid in all program futures, while still allowing objects to
attain new stronger typestates. The system is powerful enough to
establish properties of circular data structures."
}
@InProceedings{FahndrichX2007,
author = "Manuel F{\"a}hndrich and Songtao Xia",
authorASCII = "Manuel Fahndrich and Songtao Xia",
title = "Establishing object invariants with delayed types",
crossref = "OOPSLA2007",
pages = "337--350",
}
@InProceedings{SummersM2011,
author = "Summers, Alexander J. and M{\"u}ller, Peter",
authorASCII = "Summers, Alexander J. and Muller, Peter",
authorASCII = "Summers, Alexander J. and Mueller, Peter",
title = "Freedom before commitment: A lightweight type system for object initialisation",
crossref = "OOPSLA2011",
pages = "1013--1032",
url = {https://doi.acm.org/10.1145/2048066.2048142},
}
@InProceedings{ChalinR2005,
author = "Chalin, Patrice and Rioux, Fr{\'e}d{\'e}ric",
authorASCII = "Chalin, Patrice and Rioux, Frederic",
title = "Non-null references by default in the {Java} {Modeling} {Language}",
crossref = "SAVCBS2005",
NOpages = "*",
abstract =
"Based on our experiences and those of our peers, we hypothesized that in
Java code, the majority of declarations that are of reference types are
meant to be non-null. Unfortunately, the Java Modeling Language (JML), like
most interface specification and object-oriented programming languages,
assumes that such declarations are possibly-null by default. As a
consequence, developers need to write specifications that are more verbose
than necessary in order to accurately document their module interfaces. In
practice, this results in module interfaces being left incompletely and
inaccurately specified. In this paper we present the results of a study
that confirms our hypothesis. Hence, we propose an adaptation to JML that
preserves its language design goals and that allows developers to specify
that declarations of reference types are to be interpreted as non-null by
default. We explain how this default is safer and results in less writing
on the part of specifiers than null-by-default. The paper also reports on
an implementation of the proposal in some of the JML tools.",
}
@TechReport{ChalinJ2006,
author = "Patrice Chalin and Perry James",
title = "Non-null references by default in {Java}: Alleviating the nullity annotation burden",
institution = "Concordia University",
year = 2006,
type = "ENCS-CSE",
number = "2006-003",
address = Montreal,
month = dec,
note = "Revision 3s",
supersededby = "ChalinJ2007",
}
@InProceedings{ChalinJ2007,
author = "Patrice Chalin and Perry R. James",
title = "Non-null references by default in {Java}: Alleviating the nullity annotation burden",
crossref = "ECOOP2007",
pages = "227--247",
abstract =
"With Java 5 annotations, we note a marked increase in tools that statically
detect potential null dereferences. To be effective such tools require that
developers annotate declarations with nullity modifiers and have annotated
API libraries. Unfortunately, in our experience specifying moderately large
code bases, the use of non-null annotations is more labor intensive than it
should be. Motivated by this experience, we conducted an empirical study
of 5 open source projects totaling 700 KLOC which confirms that on average,
3/4 of declarations are meant to be non-null, by design. Guided by these
results, we propose adopting a non-null-by-default semantics. This new
default has advantages of better matching general practice, lightening
developer annotation burden and being safer. We adapted the Eclipse JDT
Core to support the new semantics, including the ability to read the
extensive API library specifications written in the Java Modeling Language
(JML\@). Issues of backwards compatibility are addressed.",
}
@Article{ChalinJR2008,
author = "P. Chalin and P.R. James and F. Rioux",
title = "Reducing the use of nullable types through non-null by default and monotonic non-null",
journal = "IET Software",
year = 2008,
volume = 2,
number = 6,
pages = "515--531",
month = dec,
abstract =
"With Java 5 annotations, the authors note a marked increase in tools that
can statically detect potential null dereferences. To be effective, such
tools require that developers annotate declarations with nullity modifiers
and have annotated API libraries. Unfortunately, in the experience of the
authors, specifying moderately large code bases, the use of non-null
annotations is more labour intensive than it should be. Motivated by this
experience, the authors conducted an empirical study of five open source
projects totalling 700K lines-of-code, which confirms that, on average, 75\%
of reference declarations are meant to be non-null, by design. Guided by
these results, the authors propose the adoption of non-null-by-default
semantics. This new default has advantages of better matching general
practice, lightening developer annotation burden and being safer. The
authors also describe the Eclipse Java Modelling Language (JML) Java
Development Tooling (JDT), a tool supporting the new semantics, including
the ability to read the extensive API library specifications written in the
JML. Issues of backwards compatibility are addressed. In a second phase of
the empirical study, the authors analysed the uses of null and noted that
over half of the nullable field references are only assigned non-null
values. For this category of reference, the authors introduce the concept
of monotonic non-null type and illustrate the benefits of its use.",
}
@TechReport{ChalinJK2007,
author = "Patrice Chalin and Perry R. James and George Karabotsos",
title = "The architecture of {JML4}, a proposed integrated verification environment for {JML}",
institution = "Concordia University",
year = 2007,
type = "ENCS-CSE",
number = "2007-006",
month = may,
note = "Revision 1",
}
@InProceedings{CieleckiFJJ2006,
author = "Maciej Cielecki and J\c{e}drzej Fulara and Krzysztof Jakubczyk and {\L}ukasz Jancewicz and Jacek Chrzaszcz and Aleksy Schubert and {\L}ukasz Kami{\'n}ski",
authorASCII = "Maciej Cielecki and Jedrzej Fulara and Krzysztof Jakubczyk and Lukasz Jancewicz and Jacek Chrzaszcz and Aleksy Schubert and Lukasz Kaminski",
title = "Propagation of {JML} non-null annotations in {Java} programs",
crossref = "PPPJ2006",
pages = "135--140",
abstract =
"Development of high quality code is notably difficult. Tools that help
maintaining the proper quality of code produced by programmers can be very
useful: they may increase the quality of produced software and help
managers to ensure that the product is ready for the market. One of such
tools is ESC/Java2, a static checker of Java Modeling Language
annotations. These annotations can be used to ensure that a certain
assertion is satisfied during the execution of the program, among the
others --- to ensure that a certain variable never has a null
value. Unfortunately, using ESC/Java2 can be very troublesome and
time-consuming for programmers, as it lacks a friendly user interface and a
function that propagates annotations. We present CANAPA, a tool that can
highly reduce time and effort of eliminating null pointer exceptions in
Java code. This tool can automatically propagate JML non-null annotations
and comes with a handy Eclipse plug-in. We believe that functionality of
CANAPA will minimize the effort required to benefit from using the JML
non-null checking.",
}
@PhdThesis{Ekman2006,
author = "Torbj{\"o}rn Ekman",
authorASCII = "Torbjorn Ekman",
title = "Extensible compiler construction",
school = "Lund University Department of Computer Science",
year = 2006,
address = "Lund, Sweden",
}
@InProceedings{EkmanH2007:JastAdd,
author = "Torbj{\"o}rn Ekman and G{\"o}rel Hedin",
authorASCII = "Torbjorn Ekman and Gorel Hedin",
title = "The {JastAdd} extensible {Java} compiler",
crossref = "OOPSLA2007",
pages = "1--18",
}
@Article{EkmanH2007:NonNull,
author = "Torbj{\"o}rn Ekman and G{\"o}rel Hedin",
authorASCII = "Torbjorn Ekman and Gorel Hedin",
title = "Pluggable checking and inferencing of non-null types for {Java}",
journal = JOT,
year = 2007,
volume = 6,
number = 9,
pages = "455--475",
month = oct,
abstract =
"We have implemented a non-null type checker for Java and a new non-null
inferencing algorithm for analyzing legacy code. The tools are modular
extensions to the JastAdd extensible Java compiler, illustrating how
pluggable type systems can be achieved. The resulting implementation is
compact, less than 230 lines of code for the non-null checker and 460
for the inferencer. Non-null checking is a local analysis with little
effect on compilation time. The inferencing algorithm is a
whole-program analysis, yet it runs sufficiently fast for practical
use, less than 10 seconds for 100.000 lines of code. We ran our
inferencer on a large part of the JDK library, and could detect that
around 70\% of the dereferences, and around 24\% of the method return
values, were guaranteed to be non-null.",
}
@MastersThesis{Engelen2006,
author = "Arnout F. M. Engelen",