Update docs.

emina · Jul 4, 2023 · 649184f · 649184f
1 parent 15647f2
commit 649184f
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 6 deletions.
diff --git a/rosette/guide/scribble/refs.scrbl b/rosette/guide/scribble/refs.scrbl
@@ -9,21 +9,28 @@
 
 @(define rosette:onward13
    (make-bib
-     #:title @hyperlink["http://homes.cs.washington.edu/~emina/pubs/rosette.onward13.pdf"]{Growing Solver-Aided Languages with Rosette}
+     #:title @hyperlink["http://dl.acm.org/citation.cfm?id=2509586"]{Growing Solver-Aided Languages with Rosette}
      #:author (authors "Emina Torlak" "Rastislav Bodik")
      #:date 2013
      #:location "New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!)"))
 
 @(define rosette:pldi14
    (make-bib
-    #:title @hyperlink["http://homes.cs.washington.edu/~emina/pubs/rosette.pldi14.pdf"]{A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages}
+    #:title @hyperlink["http://dl.acm.org/citation.cfm?id=2594340"]{A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages}
     #:author (authors "Emina Torlak" "Rastislav Bodik")
     #:date 2014
     #:location "Programming Language Design and Implementation (PLDI)"))
 
 @(define sympro:oopsla18
    (make-bib
-    #:title @hyperlink["https://unsat.cs.washington.edu/papers/bornholt-sympro.pdf"]{Finding Code That Explodes Under Symbolic Evaluation}
+    #:title @hyperlink["https://dl.acm.org/citation.cfm?id=3276519"]{Finding Code That Explodes Under Symbolic Evaluation}
     #:author (authors "James Bornholt" "Emina Torlak")
     #:date 2018
-    #:location "Object Oriented Programming, Systems, Languages, and Applications (OOPSLA)"))
+    #:location "Object Oriented Programming, Systems, Languages, and Applications (OOPSLA)"))
+
+@(define rosette:popl22
+   (make-bib
+    #:title @hyperlink["https://doi.org/10.1145/3498709"]{A Formal Foundation for Symbolic Evaluation with Merging}
+    #:author (authors "Sorawee Porncharoenwase" "Luke Nelson" "Xi Wang" "Emina Torlak")
+    #:date 2022
+    #:location "Principles of Programming Languages (POPL)"))
diff --git a/rosette/guide/scribble/unsafe/unsafe.scrbl b/rosette/guide/scribble/unsafe/unsafe.scrbl
@@ -4,7 +4,7 @@
 @(require (for-label rosette/base/form/define rosette/query/query rosette/solver/solution
                      (only-in rosette/base/base assert vc-true? vc) )
           racket/runtime-path racket/sandbox)
-@(require (only-in "../refs.scrbl" ~cite rosette:pldi14))
+@(require (only-in "../refs.scrbl" ~cite rosette:pldi14 rosette:popl22))
 @(require "../util/lifted.rkt")
 
 @(define-runtime-path root ".")
@@ -19,7 +19,7 @@ functionality}.  In this chapter, we briefly discuss the @racketmodname[rosette]
 dialect of the language, which exports all of Racket.  
 
 Safe use of the full @racketmodname[rosette] language requires a basic understanding
-of how Rosette's Symbolic Virtual Machine (SVM) works  @~cite[rosette:pldi14].  
+of how Rosette's Symbolic Virtual Machine (SVM) works  @~cite[rosette:pldi14 rosette:popl22].  
 Briefly, the SVM hijacks the normal Racket execution for all procedures and 
 constructs that are exported by @racketmodname[rosette/safe].  Any programs that are
 implemented exclusively in the @racketmodname[rosette/safe] language are therefore