-
Notifications
You must be signed in to change notification settings - Fork 337
/
Copy pathpapers.yml
1526 lines (1526 loc) · 66.4 KB
/
papers.yml
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
papers:
- title: "Retrofitting Parallelism onto OCaml"
publication: International Conference on Functional Programming (ICFP)
abstract: >
OCaml is an industrial-strength, multi-paradigm programming language,
widely used in industry and academia. OCaml is also one of the
few modern managed system programming languages to lack support
for shared memory parallel programming. This paper describes the design,
a full-fledged implementation and evaluation of a mostly-concurrent
garbage collector (GC) for the multicore extension of the
OCaml programming language. Given that we propose to add parallelism
to a widely used programming language with millions of lines of
existing code, we face the challenge of maintaining backwards
compatibility -- not just in terms of the language features but also the
performance of single-threaded code running with the new GC.
To this end, the paper presents a series of novel techniques and
demonstrates that the new GC strikes a balance between performance
and feature backwards compatibility for sequential programs
and scales admirably on modern multicore processors.
authors:
- KC Sivaramakrishnan
- Stephen Dolan
- Leo White
- Sadiq Jaffer
- Tom Kelly
- Anmol Sahoo
- Sudha Parimala
- Atul Dhiman
- Anil Madhavapeddy
tags:
- ICFP
- multicore
year: 2020
links:
- description: "Download PDF"
uri: https://dl.acm.org/doi/10.1145/3408995
featured: false
- title: "Bounding Data Races in Space and Time"
publication: Programming Language Design and Implementation (PLDI)
abstract: >
We propose a new semantics for shared-memory parallel
programs that gives strong guarantees even in the presence
of data races. Our local data race freedom property guar-
antees that all data-race-free portions of programs exhibit
sequential semantics. We provide a straightforward oper-
ational semantics and an equivalent axiomatic model, and
evaluate an implementation for the OCaml programming
language. Our evaluation demonstrates that it is possible to
balance a comprehensible memory model with a reasonable
(no overhead on x86, ~0.6% on ARM) sequential performance
trade-off in a mainstream programming language
authors:
- Stephen Dolan
- KC Sivaramakrishnan
- Anil Madhavapeddy
tags:
- PLDI
- multicore
year: 2018
links:
- description: "Download PDF"
uri: http://kcsrk.info/papers/pldi18-memory.pdf
featured: true
- title: "Retrofitting Effect Handlers Onto OCaml"
publication: Programming Language Design and Implementation (PLDI)
abstract: >
Effect handlers have been gathering momentum as a mechanism for modular
programming with user-defined effects. Effect handlers allow for non-local
control flow mechanisms such as generators, async/await, lightweight threads,
and coroutines to be composably expressed. We present a design and evaluate
a full-fledged efficient implementation of effect handlers for OCaml, an
industrial-strength multi-paradigm programming language. Our implementation
strives to maintain the backwards compatibility and performance profile of
existing OCaml code. Retrofitting effect handlers onto OCaml is challenging
since OCaml does not currently have any non-local control flow mechanisms
other than exceptions. Our implementation of effect handlers for OCaml:
(i) imposes a mean 1% overhead on a comprehensive macro benchmark suite
that does not use effect handlers;
(ii) remains compatible with program analysis tools that inspect the
stack;
and (iii) is efficient for new code that makes use of effect handlers.
authors:
- K. C. Sivaramakrishnan
- Stephen Dolan
- Leo White
- Tom Kelly
- Sadiq Jaffer
- Anil Madhavapeddy
tags:
- PLDI
- effects
year: 2021
links:
- description: "Download PDF"
uri: https://dl.acm.org/doi/10.1145/3453483.3454039
featured: true
- title: "Cosmo : A Concurrent Separation Logic for Multicore OCaml"
publication: International Conference on Functional Programming (ICFP)
abstract: >
Multicore OCaml extends OCaml with support for shared-memory concurrency.
It is equipped with a weak memory model, for which an operational
semantics has been published. This begs the question: what reasoning rules
can one rely upon while writing or verifying Multicore OCaml code?
To answer it, we instantiate Iris, a modern descendant of Concurrent
Separation Logic, for Multicore OCaml. This yields a low-level program
logic whose reasoning rules expose the details of the memory model.
On top of it, we build a higher-level logic, Cosmo, which trades off some
expressive power in return for a simple set of reasoning rules that allow
accessing nonatomic locations in a data-race-free manner, exploiting the
sequentially-consistent behavior of atomic locations, and exploiting the
release/acquire behavior of atomic locations.
Cosmo allows both low-level reasoning, where the details of the Multicore
OCaml memory model are apparent, and high-level reasoning, which is
independent of this memory model. We illustrate this claim via a number of
case studies: we verify several implementations of locks with respect to a
classic, memory-model-independent specification. Thus, a coarse-grained
application that uses locks as the sole means of synchronisation can be
verified in the Concurrent-Separation-Logic fragment of Cosmo, without
any knowledge of the weak memory model.
authors:
- Glen Mével
- Jacques-Henri Jourdan
- François Pottier
tags:
- icfp
- multicore
year: 2020
links:
- description: "Download PDF"
uri: https://doi.org/10.1145/3408978
featured: false
- title: "Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model"
publication: International Conference on Functional Programming (ICFP)
abstract: >
We use Cosmo, a modern concurrent separation logic, to formally specify
and verify an implementation of a multiple-producer multiple-consumer
concurrent queue in the setting of the Multicore OCaml weak memory model.
We view this result as a demonstration and experimental verification of
the manner in which Cosmo allows modular and formal reasoning about
advanced concurrent data structures. In particular, we show how the joint
use of logically atomic triples and of Cosmo's views makes it possible to
describe precisely in the specification the interaction between the queue
library and the weak memory model.
authors:
- Glen Mével
- Jacques-Henri Jourdan
tags:
- icfp
- multicore
year: 2021
links:
- description: "Download PDF"
uri: https://doi.org/10.1145/3473571
featured: false
- title: "A Separation Logic for Effect Handlers"
publication: Principles of Programming Languages (POPL)
abstract: >
User-defined effects and effect handlers are advertised and advocated as a
relatively easy-to-understand and modular approach to delimited control.
They offer the ability of suspending and resuming a computation and allow
information to be transmitted both ways between the computation, which
requests a certain service, and the handler, which provides this service.
Yet, a key question remains, to this day, largely unanswered: how does
one modularly specify and verify programs in the presence of both
user-defined effect handlers and primitive effects, such as heap-allocated
mutable state? We answer this question by presenting a Separation Logic
with built-in support for effect handlers, both shallow and deep. The
specification of a program fragment includes a protocol that describes the
effects that the program may perform as well as the replies that it can
expect to receive. The logic allows local reasoning via a frame rule and a
bind rule. It is based on Iris and inherits all of its advanced features,
including support for higher-order functions, user-defined ghost state,
and invariants. We illustrate its power via several case studies,
including (1) a generic formulation of control inversion, which turns a
producer that ``pushes'' elements towards a consumer into a producer from
which one can ``pull'' elements on demand, and (2) a simple system for
cooperative concurrency, where several threads execute concurrently, can
spawn new threads, and communicate via promises.
authors:
- Paulo Emílio de Vilhena
- François Pottier
tags:
- popl
- effects
year: 2021
links:
- description: "Download PDF"
uri: https://doi.org/10.1145/3434314
featured: false
- title: "A Memory Model for Multicore OCaml"
publication: International Conference on Functional Programming (ICFP)
abstract: >
We propose a memory model for OCaml, broadly following the design of axiomatic
memory models for languages such as C++ and Java, but with a number of
differences to provide stronger guarantees and easier reasoning to the programmer,
at the expense of not admitting every possible optimisation.
authors:
- Stephen Dolan
- KC Sivaramakrishnan
tags:
- ocaml-workshop
- multicore
year: 2017
links:
- description: "Download PDF"
uri: https://kcsrk.info/papers/memory_model_ocaml17.pdf
featured: false
- title: "Extending OCaml's `open`"
publication: Open Publishing Association
abstract: >
We propose a harmonious extension of OCaml's `open` construct.
OCaml's existing construct `open M` imports the names exported by the module `M` into the current scope.
At present `M` is required to be the path to a module. We propose extending `open` to instead accept an arbitrary module expression,
making it possible to succinctly address a number of existing scope-related difficulties that arise when writing OCaml programs.
authors:
- Runhang Li
- Jeremy Yallop
tags:
- ocaml-workshop
- core
- language
year: 2019
links:
- description: "Download PDF"
uri: https://arxiv.org/pdf/1905.06543.pdf
featured: true
- title: "Eff Directly in OCaml"
publication: Open Publishing Association
abstract: >
The language Eff is an OCaml-like language serving as a prototype implementation
of the theory of algebraic effects, intended for experimentation with algebraic
effects on a large scale.
We present the embedding of Eff into OCaml, using the library of delimited
continuations or the Multicore OCaml branch. We demonstrate the correctness of
the embedding denotationally, relying on the tagless-final-style interpreter-based
denotational semantics, including the novel, direct denotational semantics of
multi-prompt delimited control. The embedding is systematic, lightweight, performant,
and supports even higher-order, 'dynamic' effects with their polymorphism.
OCaml thus may be regarded as another implementation of Eff, broadening the
scope and appeal of that language.
authors:
- Oleg Kiselyov
- KC Sivaramakrishnan
tags:
- ocaml-workshop
- core
- language
year: 2016
links:
- description: "Download PDF"
uri: https://arxiv.org/pdf/1812.11664.pdf
featured: false
- title: "A Syntactic Approach to Type Soundness"
publication: Information & Computation, 115(1):38−94
abstract: >
This paper describes the semantics and the type system of Core ML and
uses a simple syntactic technique to prove that well-typed programs cannot
go wrong.
authors:
- Andrew K. Wright
- Matthias Felleisen
tags:
- core
- language
year: 1994
links:
- description: "Download PostScript"
uri: https://www.cs.rice.edu/CS/PLT/Publications/Scheme/ic94-wf.ps.gz
featured: false
- title: "The Essence of ML Type Inference"
publication: Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, MIT Press
abstract: >
This book chapter gives an in-depth abstract of the Core ML type system,
with an emphasis on type inference. The type inference algorithm is
described as the composition of a constraint generator, which produces a
system of type equations, and a constraint solver, which is presented as
a set of rewrite rules.
authors:
- François Pottier
- Didier Rémy
tags:
- core
- language
year: 2005
links:
- description: "Download PostScript"
uri: https://cristal.inria.fr/attapl/preversion.ps.gz
featured: false
- title: "Relaxing the Value Restriction"
publication: International Symposium on Functional and Logic Programming
abstract: >
This paper explains why it is sound to generalise certain type variables
at a `let` binding, even when the expression that is being `let`-bound is
not a value. This relaxed version of Wright's classic “value restriction”
was introduced in OCaml 3.07.
authors:
- Jacques Garrigue
tags:
- core
- language
year: 2004
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.ps.gz
featured: false
- title: "Manifest Types, Modules, and Separate Compilation"
publication: Principles of Programming Languages
abstract: >
This paper presents a variant of the Standard ML module system that
introduces a strict distinction between abstract and manifest types. The
latter are types whose definitions explicitly appear as part of a module
interface. This proposal is meant to retain most of the expressive power
of the Standard ML module system, while providing much better support
for separate compilation. This work sets the formal bases for OCaml's
module system.
authors:
- Xavier Leroy
tags:
- core
- language
- modules
year: 1994
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/xleroy-manifest_types-popl94.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/xleroy-manifest_types-popl94.ps.gz
- description: "Download DVI"
uri: https://caml.inria.fr/pub/papers/xleroy-manifest_types-popl94.dvi.gz
featured: false
- title: "Applicative Functors and Fully Transparent Higher-Order Modules"
publication: Principles of Programming Languages
abstract: >
This work extends the above paper by introducing so-called applicative
functors, that is, functors that produce compatible abstract types when
applied to provably equal arguments. Applicative functors are also a
feature of OCaml.
authors:
- Xavier Leroy
tags:
- core
- language
- modules
year: 1995
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/xleroy-applicative_functors-popl95.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/xleroy-applicative_functors-popl95.ps.gz
- description: "Download DVI"
uri: https://caml.inria.fr/pub/papers/xleroy-applicative_functors-popl95.dvi.gz
featured: false
- title: "A Modular Module System"
publication: Journal of Functional Programming, 10(3):269-303
abstract: >
This accessible paper describes a simplified implementation of the OCaml
module system, emphasizing the fact that the module system is largely
independent of the underlying core language. This is a good tutorial to
learn both how modules can be used and how they are typechecked.
authors:
- Xavier Leroy
tags:
- core
- language
- modules
year: 2000
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/xleroy-modular_modules-jfp.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/xleroy-modular_modules-jfp.ps.gz
- description: "Download DVI"
uri: https://caml.inria.fr/pub/papers/xleroy-modular_modules-jfp.dvi.gz
featured: false
- title: "A Proposal for Recursive Modules in Objective Caml"
publication: Unpublication
abstract: >
This note describes the experimental recursive modules introduced in OCaml
3.07.
authors:
- Xavier Leroy
tags:
- core
- language
- modules
year: 2003
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/xleroy-recursive_modules-03.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/xleroy-recursive_modules-03.ps.gz
featured: false
- title: "Objective ML: An Effective Object-Oriented Extension to ML"
publication: Theory and Practice of Objects Systems, 4(1):27−50
abstract: >
This paper provides theoretical foundations for OCaml's object-oriented
layer, including dynamic and static semantics.
authors:
- Didier Rémy
- Jérôme Vouillon
tags:
- core
- language
- objects
year: 1998
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/remy_vouillon-objective_ml-tapos98.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/remy_vouillon-objective_ml-tapos98.ps.gz
- description: "Download DVI"
uri: https://caml.inria.fr/pub/papers/remy_vouillon-objective_ml-tapos98.dvi.gz
featured: false
- title: "Extending ML with Semi-Explicit Higher-Order Polymorphism"
publication: Information & Computation, 155(1/2):134−169
abstract: >
This paper proposes a device for re-introducing first-class polymorphic
values into ML while preserving its type inference mechanism. This
technology underlies OCaml's polymorphic methods.
authors:
- Jacques Garrigue
- Didier Rémy
tags:
- core
- language
- objects
year: 1999
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/garrigue_remy-poly-ic99.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/garrigue_remy-poly-ic99.ps.gz
- description: "Download DVI"
uri: https://caml.inria.fr/pub/papers/garrigue_remy-poly-ic99.dvi.gz
featured: false
- title: "Programming with Polymorphic Variants"
publication: ML Workshop
abstract: >
This paper briefly explains what polymorphic variants are about and how
they are compiled.
authors:
- Jacques Garrigue
tags:
- core
- language
- polymorphic variants
year: 1998
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/garrigue-polymorphic_variants-ml98.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/garrigue-polymorphic_variants-ml98.ps.gz
featured: false
- title: "Code Reuse Through Polymorphic Variants"
publication: Workshop on Foundations of Software Engineering
abstract: >
This short paper explains how to design a modular, extensible interpreter
using polymorphic variants.
authors:
- Jacques Garrigue
tags:
- core
- language
- polymorphic variants
year: 2000
links:
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/garrigue-variant-reuse-2000.ps.gz
featured: false
- title: "Simple Type Inference for Structural Polymorphism"
publication: Workshop on Foundations of Object-Oriented Languages
abstract: >
This paper explains most of the typechecking machinery behind polymorphic
variants. At its heart is an extension of Core ML's type discipline with
so-called local constraints.
authors:
- Jacques Garrigue
tags:
- core
- language
- polymorphic variants
year: 2002
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/garrigue-structural_poly-fool02.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/garrigue-structural_poly-fool02.ps.gz
featured: false
- title: "Typing Deep Pattern-matching in Presence of Polymorphic Variants"
publication: JSSST Workshop on Programming and Programming Languages
abstract: >
This paper provides more details about the technical machinery behind
polymorphic variants, focusing on the rules for typechecking deep pattern
matching constructs.
authors:
- Jacques Garrigue
tags:
- core
- language
- polymorphic variants
year: 2004
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/garrigue-deep-variants-2004.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/garrigue-deep-variants-2004.ps.gz
featured: false
- title: "Labeled and Optional Arguments for Objective Caml"
publication: JSSST Workshop on Programming and Programming Languages
abstract: >
This paper offers a dynamic semantics, a static semantics, and a
compilation scheme for OCaml's labeled and optional function parameters.
authors:
- Jacques Garrigue
tags:
- core
- language
year: 2001
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/garrigue-labels-ppl01.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/garrigue-labels-ppl01.ps.gz
- description: "Download DVI"
uri: https://caml.inria.fr/pub/papers/garrigue-labels-ppl01.dvi.gz
featured: false
- title: "Meta-Programming Tutorial with CamlP4"
publication: Commercial Users of Functional Programming
abstract: Meta-programming tutorial with Camlp4
authors:
- Jake Donham
tags:
- core
- language
year: 2010
links:
- description: "View Online"
uri: https://github.com/jaked/cufp-metaprogramming-tutorial
featured: false
- title: "The ZINC Experiment, an Economical Implementation of the ML Language"
publication: Technical report 117, INRIA
abstract: >
This report contains a abstract of the ZINC compiler, which later evolved
into Caml Light, then into OCaml. Large parts of this report are out of
date, but it is still valuable as a abstract of the abstract machine used
in Caml Light and (with some further simplifications and speed
improvements) in OCaml.
authors:
- Xavier Leroy
tags:
- compiler
- runtime
year: 1990
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/xleroy-zinc.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/xleroy-zinc.ps.gz
featured: false
- title: "The Effectiveness of Type-based Unboxing"
publication: Workshop on Types in Compilation
abstract: >
This paper surveys and compares several data representation strategies,
including the one used in the OCaml native-code compiler.
authors:
- Xavier Leroy
tags:
- compiler
- runtime
year: 1997
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/xleroy-unboxing-tic97.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/xleroy-unboxing-tic97.ps.gz
featured: false
- title: "A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML"
publication: Principles of Programming Languages
abstract: >
Superseded by "Portable, Unobtrusive Garbage Collection for Multiprocessor
Systems"
authors:
- Damien Doligez
- Xavier Leroy
tags:
- garbage collection
- runtime
year: 1993
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/doligez_xleroy-concurrent_gc-popl93.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/doligez_xleroy-concurrent_gc-popl93.ps.gz
featured: false
- title: "Portable, Unobtrusive Garbage Collection for Multiprocessor Systems"
publication: Principles of Programming Languages
abstract: >
This paper describes a concurrent version of the garbage collector found
in Caml Light and OCaml's runtime system.
authors:
- Damien Doligez
- Georges Gonthier
tags:
- garbage collection
- runtime
year: 1994
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/doligez_gonthier-gc-popl94.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/doligez_gonthier-gc-popl94.ps.gz
featured: false
- title: "Conception, Réalisation et Certification d'un Glaneur de Cellules Concurrent"
publication: Ph.D. thesis, Université Paris 7
abstract: >
All you ever wanted to know about the garbage collector found in Caml
Light and OCaml's runtime system.
authors:
- Damien Doligez
- Georges Gonthier
tags:
- garbage collection
- runtime
year: 1995
links:
- description: "Download PDF"
uri: https://caml.inria.fr/pub/papers/doligez-these.pdf
- description: "Download PostScript"
uri: https://caml.inria.fr/pub/papers/doligez-these.ps.gz
featured: false
- title: "Optimizing Pattern Matching"
publication: Proceedings of the sixth ACM SIGPLAN International Conference on Functional Programming (ICFP)
abstract: >
All you ever wanted to know about the garbage collector found in Caml
Light and OCaml's runtime system.
authors:
- Fabrice Le Fessant
- Luc Maranget
tags:
- pattern-matching
- runtime
year: 2001
links:
- description: "View Online"
uri: https://dl.acm.org/citation.cfm?id=507641
featured: false
- title: "OCaml for the Masses"
publication: ACM Queue
abstract: >
Why the next language you learn should be functional.
authors:
- Yaron Minsky
tags:
- industrial
year: 2011
links:
- description: "View Online"
uri: https://queue.acm.org/detail.cfm?id=2038036
featured: false
- title: "Xen and the Art of OCaml"
publication: Commercial Users of Functional Programming (CUFP)
abstract: >
In this talk, we will firstly describe the architecture of XenServer and
the XenAPI and discuss the challenges faced with implementing an
Objective Caml based solution. These challenges range from the low-level
concerns of interfacing with Xen and the Linux kernel, to the high-level
algorithmic problems such as distributed failure planning. In addition, we
will discuss the challenges imposed by using OCaml in a commercial
environment, such as supporting product upgrades, enhancing
supportability, and scaling the development team.
authors:
- Anil Madhavapeddy
tags:
- industrial
- application
year: 2008
links:
- description: "Download PDF"
uri: https://cufp.org/archive/2008/slides/MadhavapeddyAnil.pdf
featured: false
- title: "Chemoinformatics and Structural Bioinformatics in OCaml"
publication: Journal of Cheminformatics
abstract: >
In this article, we share our experience in prototyping chemoinformatics
and structural bioinformatics software in OCaml
authors:
- François Berenger
- Kam Y. J. Zhang
- Yoshihiro Yamanishi
tags:
- industrial
- application
- bioinformatics
year: 2019
links:
- description: "View Online"
uri: https://jcheminf.biomedcentral.com/articles/10.1186/s13321-019-0332-0
featured: false
- title: "A Declarative Syntax Definition for OCaml"
publication: International Conference on Functional Programming (ICFP)
abstract: >
In this talk we present our work on a syntax definition for the OCaml
language in the syntax definition formalism SDF3. SDF3 supports
high-level definition of concrete and abstract syntax through declarative
disambiguation and definition of constructors, enabling a direct mapping
to abstract syntax. Based on the SDF3 syntax definition, the Spoofax
language workbench produces a complete syntax aware editor with a parser,
syntax checking, parse error recovery, syntax highlighting, formatting
with correct parenthesis insertion, and syntactic completion. The syntax
definition should provide a good basis for experiments with the design of
OCaml and the development of further tooling. In the talk we will
highlight interesting aspects the syntax definition, discuss issues we
encountered in the syntax of OCaml, and demonstrate the editor.
authors:
- Luis Eduardo de Souza Amorim
- Eelco Visser
tags:
- ocaml-workshop
year: 2020
links:
- description: "View Online"
uri: https://eelcovisser.org/talks/2020/08/28/ocaml/
featured: false
- title: "A Simple State-Machine Framework for Property-Based Testing in OCaml"
publication: International Conference on Functional Programming (ICFP)
abstract: >
Since their inception state-machine frameworks have proven their worth by
finding defects in everything from the underlying AUTOSAR components of
Volvo cars to digital invoicing sys- tems. These case studies were
carried out with Erlang’s commercial QuickCheck state-machine framework
from Quviq, but such frameworks are now also available for Haskell, F#,
Scala, Elixir, Java, etc. We present a typed state-machine framework for
OCaml based on the QCheck library and illustrate a number concepts common
to all such frameworks: state modeling, commands, interpreting commands,
preconditions, and agreement checking.
authors:
- Jan Midtgaard
tags:
- ocaml-workshop
year: 2020
links:
- description: "Download PDF"
uri: https://janmidtgaard.dk/papers/Midtgaard%3AOCaml20.pdf
featured: false
- title: "AD-OCaml: Algorithmic Differentiation for OCaml"
publication: International Conference on Functional Programming (ICFP)
abstract: >
AD-OCaml is a library framework for calculating mathematically exact
derivatives and deep power series approximations of almost arbitrary
OCaml programs via algorithmic differentiation. Unlike similar
frameworks, this includes programs with side effects, aliasing, and
programs with nested derivative operators. The framework also offers
implicit parallelisation of both user programs and their transformations.
The presentation will provide a short introduction to the mathematical
problem, the difficulties of implementing a solution, the design of the
library, and a demonstration of its capabilities.
authors:
- Markus Mottl
tags:
- ocaml-workshop
year: 2020
links:
- description: "View Online"
uri: https://icfp20.sigplan.org/details/ocaml-2020-papers/12/AD-OCaml-Algorithmic-Differentiation-for-OCaml
featured: false
- title: "API Migration: Compare Transformed"
publication: International Conference on Functional Programming (ICFP)
abstract: >
In this talk we describe our experience in using an automatic
API-migration strategy dedicated at changing the signatures of OCaml
functions, using the Rotor refactoring tool for OCaml. We perform a case
study on open source Jane Street libraries by using Rotor to refactor
comparison functions so that they return a more precise variant type
rather than an integer. We discuss the difficulties of refactoring the
Jane Street code base, which makes extensive use of PPX macros, and
ongoing work implementing new refactorings.
authors:
- Joseph Harrison
- Steven Varoumas
- Simon Thompson
- Reuben Rowe
tags:
- ocaml-workshop
year: 2020
links:
- description: "View Online"
uri: https://icfp20.sigplan.org/details/ocaml-2020-papers/7/API-migration-compare-transformed
- description: "Download PDF"
uri: https://www.cs.kent.ac.uk/people/staff/sjt/Pubs/OCaml_workshop2020.pdf
featured: false
- title: "Irmin v2"
publication: International Conference on Functional Programming (ICFP)
abstract: >
Irmin is an OCaml library for building distributed databases with the same
design principles as Git. Existing Git users will find many familiar
features: branching/merging, immutable causal history for all changes,
and the ability to restore to any previous state. Irmin v2 adds new
accessibility methods to the store: we can now use Irmin from a CLI, or
in a browser using `irmin-graphql`. It also has a new backend, `irmin-pack`,
which is optimised for space usage and is used by the Tezos blockchain.
authors:
- Clément Pascutto
- Ioana Cristescu
- Craig Ferguson
- Thomas Gazagnaire
- Romain Liautaud
tags:
- ocaml-workshop
year: 2020
links:
- description: "View Online"
uri: https://icfp20.sigplan.org/details/ocaml-2020-papers/10/Irmin-v2
- description: "View Online"
uri: https://tarides.com/blog/2019-11-21-irmin-v2
featured: false
- title: "LexiFi Runtime Types"
publication: International Conference on Functional Programming (ICFP)
abstract: >
LexiFi maintains an OCaml compiler extension that enables introspection
through runtime type representations. Recently, we implemented a syntax
extension (PPX) that enables the use of LexiFi runtime types on vanilla
compilers. We propose to present our publicly available runtime types and
their features. Most notably, we want to present a mechanism for pattern
matching on runtime types with holes.
authors:
- Patrik Keller
- Marc Lasson
tags:
- ocaml-workshop
year: 2020
links:
- description: "View Online"
uri: https://icfp20.sigplan.org/details/ocaml-2020-papers/9/LexiFi-Runtime-Types
- description: "Download PDF"
uri: https://informationsecurity.uibk.ac.at/pdfs/KL2020_LexiFi_Runtime_Types_OCAML.pdf
- description: "View Online"
uri: https://www.lexifi.com/blog/ocaml/runtime-types/
featured: false
- title: "OCaml Under the Hood: SmartPy"
publication: International Conference on Functional Programming (ICFP)
abstract: >
SmartPy is a complete system to develop smart-contracts for the Tezos
blockchain. It is an embedded EDSL in Python to write contracts and their
tests scenarios. It includes an online IDE, a chain explorer, and a
command line interface. Python is used to generate programs in an
imperative, type inferred, intermediate language called SmartML. SmartML
is also the name of the OCaml library which provides an interpreter, a
compiler to Michelson (the smart-contract language of Tezos), as well as
a scenario “on-chain” interpreter. The IDE uses a mix of OCaml built with
`js_of_ocaml` and pure Javascript. The command line interface also builds
with `js_of_ocaml` to run on Node.js.
authors:
- Sebastien Mondet
tags:
- ocaml-workshop
year: 2020
links:
- description: "View Online"
uri: https://icfp20.sigplan.org/details/ocaml-2020-papers/11/OCaml-Under-The-Hood-SmartPy
- description: "Download PDF"
uri: https://wr.mondet.org/paper/smartpy-ocaml-2020.pdf
featured: false
- title: "OCaml-CI: A Zero-Configuration CI"
publication: International Conference on Functional Programming (ICFP)
abstract: >
OCaml-CI is a CI service for OCaml projects. It uses metadata from the
project’s opam and `dune` files to work out what to build, and it uses caching
to make builds fast. It automatically tests projects against multiple
OCaml versions and OS platforms. The CI has been deployed on around 50
projects so far on GitHub, and many of them see response times an order of
magnitude quicker than with less integrated CI solutions. This talk will
introduce the CI service and then look at some of the technologies used to
build it.
authors:
- Thomas Leonard
- Craig Ferguson
- Kate Deplaix
- Magnus Skjegstad
- Anil Madhavapeddy
tags:
- ocaml-workshop
year: 2020
links:
- description: "View Online"
uri: https://icfp20.sigplan.org/details/ocaml-2020-papers/6/OCaml-CI-A-Zero-Configuration-CI
featured: false
- title: "Parallelising Your OCaml Code with Multicore OCaml"
publication: International Conference on Functional Programming (ICFP)
abstract: >
With the availability of multicore variants of the recent OCaml versions
(4.10 and 4.11) that maintain backwards compatibility with the existing
OCaml C-API, there has been increasing interest in the wider OCaml
community for parallelising existing OCaml code.
authors:
- Sadiq Jaffer
- Sudha Parimala
- KC Sivaramarkrishnan
- Tom Kelly
- Anil Madhavapeddy
tags:
- ocaml-workshop
year: 2020
links:
- description: "Download PDF"
uri: https://github.com/ocaml-multicore/multicore-talks/blob/master/ocaml2020-workshop-parallel/multicore-ocaml20.pdf
- description: "View Online"
uri: https://icfp20.sigplan.org/details/ocaml-2020-papers/5/Parallelising-your-OCaml-Code-with-Multicore-OCaml
featured: false
- title: "The ImpFS Filesystem"
publication: International Conference on Functional Programming (ICFP)
abstract: >
This proposal describes a presentation to be given at the OCaml’20
workshop. The presentation will cover a new OCaml filesystem, ImpFS, and
the related libraries. The filesystem makes use of a B-tree library
presented at OCaml’17 and a key-value store presented at ML’19. In
addition, there are a number of other support libraries that may be of
interest to the community. ImpFS represents a single point in the
filesystem design space, but we hope that the libraries we have developed
will enable others to build further filesystems with novel features.
authors:
- Tom Ridge
tags:
- ocaml-workshop
year: 2020
links:
- description: "View Online"
uri: https://icfp20.sigplan.org/details/ocaml-2020-papers/8/The-ImpFS-filesystem
featured: false
- title: "The Final Pieces of the OCaml Documentation Puzzle"
publication: International Conference on Functional Programming (ICFP)
abstract: >
`odoc` is the latest attempt at creating a documentation tool which handles
the full complexity of the OCaml language. It has been a long time coming
as tackling both the module system and rendering into rich documents makes
for a difficult task. Nevertheless we believe the two recent developments
provides the final pieces of the OCaml documentation puzzle. This two
improvements split `odoc` in two layers: a model layer, with a deep
understanding of the module system, and a document layer allowing for easy
definition of new outputs.
authors:
- Jonathan Ludlam
- Gabriel Radanne
- Leo White
tags:
- ocaml-workshop
year: 2020
links:
- description: "View Online"
uri: https://icfp20.sigplan.org/details/ocaml-2020-papers/4/The-final-pieces-of-the-OCaml-documentation-puzzle
featured: false
- title: "Types in Amber"
publication: International Conference on Functional Programming (ICFP)
abstract: >
Coda is a new cryptocurrency that uses zk-SNARKs to dramatically reduce
the size of data needed by nodes running its protocol. Nodes
communicate in a format automatically derived from type definitions in
OCaml source files. As the Coda software evolves, these formats for sent
data may change. We wish to allow nodes running older versions of the
software to communicate with newer versions. To achieve that, we identify
stable types that must not change over time, so that their serialisations
also do not change.
authors:
- Paul Steckler
- Matthew Ryan
tags:
- ocaml-workshop
year: 2020
links:
- description: "View Online"
uri: https://icfp20.sigplan.org/details/ocaml-2020-papers/3/Types-in-amber
featured: false
- title: "OCamlPro: Promoting OCaml Use in Industry"
publication: International Conference on Functional Programming (ICFP)
abstract: >
One year after the foundation of OCamlPro, Fabrice Le Fessant presents at
the OCaml Workshop a brief summary of the tasks undertaken in the span of
that fateful year. Cheat Sheets, opam package manager, and many more are
the start of a long stream of contributions for the OCaml Distribution
and Community at large.
authors:
- Fabrice le Fessant
tags:
- ocaml-workshop
year: 2012
links:
- description: "View Online"
uri: https://www.youtube.com/watch?v=DXr8Lr3z7wY&feature=plcp
featured: false
- title: "opam: An OCaml Package Manager"
publication: International Conference on Functional Programming (ICFP)
abstract: >
Six months after the start of the development of the opam package
manager, Frederick Tuong, Fabrice Le Fessant, and Thomas Gazagnaire
present for the first time what would in time become the official package
manager for the OCaml Distribution. Covering the current state of the
repository, and future prospects for the platform, this small piece of
media witholds a significant piece of history for OCaml.
authors: