refscript
Refinement Types for Scripting Languages
File Explorer
Download Latest Version (.zip)- includes.tex
- ott-local.tex
- typing.ott
- typing.tex
- rules-partial.md
- typing.txt
- listproc.sty
- Makefile
- mathpartir.sty
- ottalt.sty
- README.md
- sigplanconf.cls
- ecoop15.png
- Screenshot-from-2015-04-30-08-29-12.png
- Screenshot-from-2015-05-01-16-19-23.png
- ignores.dic
- SoCal-05-2015.html
- SoCal-05-2015.mdk
- Dagstuhl-07-2014.pdf
- Dagstuhl-07-2014.pptx
- topics.md
- Specifications.md
- flycheck-rsc.el
- tsc-refscript
- lib.d.ts
- tsc-refscript.js
- core.d.ts
- jquery.d.ts
- winjs.d.ts
- winrt.d.ts
- rsc.vim
- rsc.vim
- array.d.ts
- boolean.d.ts
- console.d.ts
- dom.d.ts
- error.d.ts
- function.d.ts
- iarguments.d.ts
- list.d.ts
- math.d.ts
- number.d.ts
- object.d.ts
- regexp.d.ts
- string.d.ts
- undefined.d.ts
- aliases.d.ts
- measures.d.ts
- mutability.d.ts
- prims.d.ts
- qualifiers.d.ts
- .gitignore
- cleanup.ts
- package.json
- README
- tsconfig.json
- tsd.json
- Annotations.hs
- Check.hs
- Syntax.hs
- EitherIO.hs
- Env.hs
- Files.hs
- Alias.hs
- CGMonad.hs
- Checker.hs
- Constraints.hs
- Environment.hs
- Qualifiers.hs
- Refinements.hs
- Types.hs
- Annotations.hs
- Common.hs
- Declarations.hs
- Lexer.hs
- Types.hs
- Annotations.hs
- ClassHierarchy.hs
- Common.hs
- Errors.hs
- Module.hs
- Symbols.hs
- Syntax.hs
- Types.hs
- SSA.hs
- SSAMonad.hs
- Checker.hs
- Environment.hs
- Sub.hs
- Subst.hs
- TCMonad.hs
- Types.hs
- Unify.hs
- Annotations.hs
- AST.hs
- ClassHierarchy.hs
- CmdLine.hs
- Constraints.hs
- Environment.hs
- Errors.hs
- Locations.hs
- Lookup.hs
- Misc.hs
- Module.hs
- Names.hs
- Parser.hs
- Pretty.hs
- Program.hs
- Symbols.hs
- SystemUtils.hs
- Transformations.hs
- Traversals.hs
- Types.hs
- TypeUtilities.hs
- Visitor.hs
- Rsc.hs
- d3.d.ts
- d3.rsc.ts
- number.ts
- ascending.ts
- descending.ts
- entries.ts
- extent.ts
- keys.ts
- max.ts
- mean.ts
- median.ts
- merge.ts
- min.ts
- pairs.ts
- permute.ts
- quantile.ts
- range.ts
- shuffle.ts
- sum.ts
- transpose.ts
- values.ts
- zip.ts
- navier-small-1.ts
- navier-small.ts
- mulThms-1.d.ts
- mulThms.d.ts
- mulThms.ts
- navier-stokes-typed-octane.ts
- raytrace-typed-octane.ts
- richards-typed-octane.ts
- splay-typed-octane.ts
- transducers.ts
- checker-1.ts
- core.defs.ts
- types.ts
- checker.ts
- core.ts
- cast.ts
- createElt.ts
- ctor.ts
- infer.ts
- minindex-classic.ts
- minindex-modern.ts
- negate.ts
- opt-args.ts
- poly.ts
- reals.ts
- string-coercion.ts
- variadic.ts
- while-rec.ts
- jquery.d.ts
- jquery.min.d.ts
- notes.md
- test0.ts
- 00-array.ts
- 01-array.ts
- 02-array.ts
- 03-array.ts
- 04-array.ts
- 05-array.ts
- 06-array.ts
- 07-array.ts
- 08-array.ts
- 09-array.ts
- 10-array.ts
- 11-array.ts
- 12-array.ts
- 13-array.ts
- 14-array.ts
- 16-array.ts
- 17-array.ts
- 18-array.ts
- 19-array.ts
- 20-array.ts
- 21-array.ts
- 22-array.ts
- 23-array.ts
- 24-array.ts
- 25-array.ts
- 00-test.ts
- 01-test.ts
- 02-test.ts
- 03-test.ts
- 00-class.ts
- 01-class.ts
- 02-class.ts
- 03-class.ts
- 04-class.ts
- 05-class.ts
- 06-class.ts
- 07-class.ts
- 08-createElt.ts
- 09-ctor.ts
- 10-ctor.ts
- 11-ctor.ts
- 12-ctor.ts
- 13-ctor.ts
- 14-ctor.ts
- 15-ctor.ts
- 16-ctor.ts
- 17-ctor.ts
- 18-ctor.ts
- 19-ctor.ts
- 20-ctor.ts
- 21-eq-val.ts
- 22-func-field-ctor.ts
- 23-inheritance.ts
- 24-init.ts
- 25-init.ts
- 26-init.ts
- 27-init.ts
- 28-interface.ts
- 29-method-mut.ts
- 31-offsets.ts
- 32-point.ts
- 33-self.ts
- 34-this-meth-scope.ts
- 35-ctor-args-missing.ts
- 01-enum.ts
- 02-enum.ts
- min-index-modern.ts
- opt-args.ts
- 00-inclusion.ts
- 01-inclusion.ts
- 03-inclusion.ts
- 04-inclusion.ts
- 05-inclusion.ts
- 06-inclusion.ts
- 07-inclusion.ts
- 08-inclusion.ts
- 09-inclusion.ts
- emp-00.ts
- list-00.ts
- list-01.ts
- list-02.ts
- list-03.ts
- list-04.ts
- list-05.ts
- list-06.ts
- list-07.ts
- list-08.ts
- list-09.ts
- list-10.ts
- list-11.ts
- list-12.ts
- listsum-00a.ts
- listsum-00b.ts
- safeappend.ts
- unfold-list-00.ts
- unfold-list-01.ts
- union-00.ts
- for-02.ts
- for-03.ts
- for-rec-01.ts
- for-rec-02.ts
- obj-00.ts
- obj-01.ts
- obj-03.ts
- obj-04.ts
- while-01.ts
- while-02.ts
- while-03.ts
- while-04.ts
- while-05.ts
- while-06.ts
- while-rec.ts
- 00-abs-sig-bad.ts
- 01-abs.ts
- 06-cousot.ts
- 08-global.ts
- 09-fixme.ts
- 12-incr.ts
- 18-inner.ts
- 19-locks.ts
- 20-locks.ts
- 26-negate.ts
- 27-negate.ts
- 28-negate.ts
- 29-negate.ts
- 33-opt-args.ts
- 36-packet.ts
- 37-poly.ts
- 38-poly.ts
- 39-poly.ts
- 40-poly.ts
- 42-unsafe-meth-call.ts
- 43-top-level.ts
- 44-twice.ts
- 49-vararg.ts
- 50-vararg.ts
- 51-vararg.ts
- 52-vararg.ts
- 53-vararg.ts
- 54-short-circuit.ts
- 55-abs-join.ts
- 56-abs-join.ts
- 57-unite.ts
- 58-unite.ts
- 59-class-inv.ts
- 61-array-map.ts
- 62-flag-narrowing.ts
- abs-hof.ts
- abs.ts
- animals-00.ts
- animals-01.ts
- animals-02.ts
- animals.ts
- apply.ts
- array-tag-check-00.ts
- array-tag-check.ts
- incr.ts
- incr3.ts
- 00-object.ts
- 01-object.ts
- 02-object.ts
- 03-object.ts
- 04-object.ts
- 05-object.ts
- 06-object.ts
- 07-object.ts
- 08-object.ts
- 09-object.ts
- 10-object.ts
- 11-object.ts
- 12-object.ts
- 13-object.ts
- 14-object.ts
- 15-object.ts
- 16-object.ts
- 17-object.ts
- 18-object.ts
- 19-object.ts
- 20-object.ts
- 21-object.ts
- opt-fields-01.ts
- string-idx-00.ts
- string-idx-01.ts
- add-03.ts
- add-03a.ts
- add-05.ts
- add-07.ts
- add-08.ts
- choice.ts
- cond-expr-00.ts
- conditional-00.ts
- conditional-01.ts
- conditional-02.ts
- id-00.ts
- id-01.ts
- inc-00.ts
- inc-01.ts
- lor-00.ts
- lor-01.ts
- lor-02.ts
- lor-03.ts
- lor-04.ts
- lor-05.ts
- lor-06.ts
- stmt-00.ts
- str-00.ts
- sum-bad.ts
- sum-badder.ts
- sum-return-missing.ts
- sum-ssa-bad.ts
- tags.ts
- test-00.ts
- test-01.ts
- test-bad-00.ts
- reals-00.ts
- reals-01.ts
- reals-02.ts
- 00-scope.ts
- 01-scope.ts
- 02-scope.ts
- 11-nested.ts
- init-01.ts
- init-02.ts
- init-03.ts
- init-04.ts
- init-06.ts
- 01-error.ts
- 02-glob.ts
- 03-glob.ts
- 04-glob.ts
- 05-glob.ts
- 06-bool.ts
- 07-bool.ts
- 08-func-expression.ts
- 09-func-expression.ts
- 10-func-expression.ts
- 11-runtime-tags.ts
- 12-unbound-tvar.ts
- 13-contextual.ts
- 21-conditional-expression.ts
- 22-unification.ts
- 24-unification.ts
- 25-field-update.ts
- 26-unification.ts
- 27-unification.ts
- 28-unification.ts
- 33-loop-ssa.ts
- 35-modules.ts
- 36-truthy.ts
- 38-meth-invariant.ts
- 40-unbound-symbol.ts
- 42-unbound-symbol.ts
- 43-func-invariant.ts
- 44-overload.ts
- 45-immutable-field.ts
- 47-overloads.ts
- 48-undead.ts
- 51-bitvector.ts
- 52-bitvector.ts
- 54-hex.ts
- 55-intersection.ts
- 57-non-linear.ts
- 60-opt-args.ts
- 61-string-coercion.ts
- 63-unif.ts
- 65-variadic.ts
- 67-return-false.ts
- bad-spec-00.ts
- cast-00.ts
- minindex-00.ts
- 46-contextual.ts
- talias-00.ts
- talias-01.ts
- talias-02.ts
- talias-03.ts
- talias-04.ts
- talias-06.ts
- test-00.ts
- test-01.ts
- test-02.ts
- test-03.ts
- test-04.ts
- test-13.ts
- test-14.ts
- test-15.ts
- 00-array.ts
- 01-array.ts
- 02-array.ts
- 03-array.ts
- 04-array.ts
- 05-array.ts
- 06-array.ts
- 07-array.ts
- 08-array.ts
- 09-array.ts
- 10-array.ts
- 11-array.ts
- 12-array.ts
- 13-array.ts
- 14-array.ts
- 15-array.ts
- 16-array.ts
- 17-array.ts
- 18-array.ts
- 19-array.ts
- 20-array.ts
- 21-array.ts
- 22-array.ts
- 23-array.ts
- 24-array.ts
- 25-array.ts
- 26-array.ts
- 00-test.ts
- 01-test.ts
- 02-test.ts
- 03-test.ts
- 04-test.ts
- 00-class.ts
- 01-class.ts
- 03-class.ts
- 04-class.ts
- 05-class.ts
- 06-class.ts
- 08-class.ts
- 09-class.ts
- 10-class.ts
- 11-class.ts
- 12-class.ts
- 13-class.ts
- 14-class.ts
- 15-classhierarchy.ts
- 16-createElt.ts
- 17-ctor.ts
- 18-ctor.ts
- 19-ctor.ts
- 20-ctor.ts
- 21-ctor.ts
- 22-ctor.ts
- 23-ctor.ts
- 24-ctor.ts
- 25-ctor.ts
- 26-ctor.ts
- 27-eq_val.ts
- 28-func-field-ctor.ts
- 29-glob-in-method.ts
- 30-implements.ts
- 31-implements.ts
- 32-inheritance.ts
- 34-init.ts
- 35-init.ts
- 36-init.ts
- 37-interface.ts
- 38-interface.ts
- 39-method.ts
- 40-mutability.ts
- 41-offsets.ts
- 42-point.ts
- 43-self.ts
- 44-subclass.ts
- 45-this-meth-scope.ts
- 00-enum.ts
- 01-enum.ts
- 02-enum.ts
- minindex-classic.ts
- minindex-modern-lib.ts
- minindex-modern.ts
- opt-args.ts
- 00-inclusion.ts
- 01-inclusion.ts
- 02-inclusion.ts
- 03-inclusion.ts
- 04-inclusion.ts
- 05-inclusion.ts
- 06-inclusion.ts
- 07-inclusion.ts
- 08-inclusion.ts
- 10-inclusion.ts
- emp-00.ts
- emp-01.ts
- list-00.ts
- list-01.ts
- list-02.ts
- list-03.ts
- list-head-01.ts
- list-head-02.ts
- listsum-00.ts
- listsum-01.ts
- listsum-02.ts
- listsum-03.ts
- map.ts
- safeappend.ts
- safehead.ts
- safemap.ts
- safereverse.ts
- unfold-list-00.ts
- unfold-list-01.ts
- union-00.ts
- double-for.ts
- for-02.ts
- for-03.ts
- for-05.ts
- for-06.ts
- for-07.ts
- for-rec.ts
- obj-00.ts
- obj-01.ts
- obj-02.ts
- while-01.ts
- while-02.ts
- while-03.ts
- while-04.ts
- while-06.ts
- while-rec.ts
- 00-abs.ts
- 01-abs-hof.ts
- 02-animals.ts
- 03-apply.ts
- 04-array-tag-check.ts
- 05-callable-interface.ts
- 06-cousot.ts
- 07-cousot.ts
- 08-cousot.ts
- 10-dep.ts
- 11-driver.ts
- 12-incr.ts
- 13-incr.ts
- 14-incr.ts
- 15-inc.ts
- 16-init.ts
- 17-init.ts
- 18-inner.ts
- 19-locks.ts
- 20-locks.ts
- 21-locks-cond.ts
- 22-max.ts
- 23-minindex.ts
- 24-minindex.ts
- 25-minindex.ts
- 26-negate.ts
- 27-negate.ts
- 28-negate.ts
- 29-negate.ts
- 30-negate.ts
- 33-opt-args.ts
- 34-opt-args.ts
- 35-overload.ts
- 36-packet.ts
- 37-poly.ts
- 38-poly.ts
- 39-poly.ts
- 40-poly.ts
- 41-poly.ts
- 42-safe-meth-call.ts
- 43-top-level.ts
- 44-twice-hof.ts
- 45-twice.ts
- 46-underscore.ts
- 47-underscore.ts
- 48-unite.ts
- 49-vararg.ts
- 50-vararg.ts
- 51-vararg.ts
- 52-vararg.ts
- 53-vararg.ts
- 54-short-circuit.ts
- 59-class-inv.ts
- 60-d3_mean.ts
- 61-array-map.ts
- 62-flag-narrowing.ts
- 00-object.ts
- 01-object.ts
- 02-object.ts
- 03-object.ts
- 06-object.ts
- 07-object.ts
- 08-object.ts
- 09-object.ts
- 10-object.ts
- 11-object.ts
- 12-object.ts
- 13-object.ts
- 14-object.ts
- 19-object.ts
- 20-object.ts
- 21-object.ts
- 22-object.ts
- hasOwnProperty.ts
- opt-fields-01.ts
- string-idx-00.ts
- add-01.ts
- add-02.ts
- add-03.ts
- add-04.ts
- add-06.ts
- add-07.ts
- cond-expr-00.ts
- cond-expr-01.ts
- id-00.ts
- id-01.ts
- id-02.ts
- inc-00.ts
- inc-02.ts
- lor-00.ts
- lor-01.ts
- lor-02.ts
- lor-03.ts
- lor-04.ts
- lor-05.ts
- lor-06.ts
- pos.ts
- stmt.ts
- str.ts
- sum-00.ts
- sum-01.ts
- sum-02.ts
- sum-infer-00.ts
- sum-infer-01.ts
- tags.ts
- unary-plus-00.ts
- reals-00.ts
- reals-01.ts
- reals-02.ts
- 00-scope.ts
- 01-scope.ts
- 02-scope.ts
- 03-scope.ts
- 04-scope.ts
- 05-scope.ts
- 06-scope.ts
- 07-scope.ts
- 08-scope.ts
- 09-scope.ts
- 10-initialization.ts
- 10-scope.ts
- 11-nested.ts
- 12-ssa.ts
- 13-nested.ts
- init-01.ts
- init-02.ts
- init-03.ts
- init-04.ts
- init-05.ts
- init-06.ts
- 00-empty.ts
- 01-error.ts
- 02-glob.ts
- 03-glob.ts
- 04-glob.ts
- 06-bool.ts
- 07-bool.ts
- 08-func-expression.ts
- 09-func-expression.ts
- 10-func-expression.ts
- 11-runtime-tags.ts
- 12-runtime-tags.ts
- 13-contextual.ts
- 14-arithmetic.ts
- 15-string-construction.ts
- 16-arguments-var.ts
- 17-absolute.ts
- 21-conditional-expression.ts
- 22-unification.ts
- 23-unification.ts
- 24-unification.ts
- 25-field-update.ts
- 26-unification.ts
- 27-unification.ts
- 28-top-type.ts
- 35-modules.ts
- 36-truthy.ts
- 37-overload.ts
- 38-overload.ts
- 39-overload.ts
- 43-func-invariant.ts
- 44-overload.ts
- 46-contextual.ts
- 47-overloads.ts
- 48-field-invariant.ts
- 49-addEntry.ts
- 50-adhoc.ts
- 51-bitvector.ts
- 52-bitvector.ts
- 54-hex.ts
- 55-intersection.ts
- 56-meth-invariant.ts
- 57-non-linear.ts
- 58-qualgen-00.ts
- 59-opt-args.ts
- 59-qualgen.ts
- 60-opt-args.ts
- 60-ref-in-constructor.ts
- 61-string-coercion.ts
- 62-tvars.ts
- 63-unif.ts
- 64-upcast.ts
- 65-bitvectors.ts
- 65-variadic.ts
- 66-bitvectors.ts
- d3-sum.ts
- 09-d3_mean.ts
- talias-00.ts
- talias-01.ts
- talias-02.ts
- talias-03.ts
- talias-04.ts
- talias-05.ts
- talias-07.ts
- talias-08.ts
- talias-09.ts
- test-00.ts
- test-01.ts
- test-02.ts
- test-03.ts
- test-04.ts
- test-05.ts
- test-06.ts
- test-07.ts
- test-08.ts
- test-09.ts
- test-10.ts
- test-12.ts
- test-13.ts
- test-14.ts
- test-15.ts
- switch-neg-00.ts
- circular-logic.ts
- bitvector-02.ts
- proto-lookup1.ts
- proto-lookup7.ts
- 66-variadic.ts
- class-07.ts
- iterable.ts
- moveable-point.ts
- break.ts
- switch-00.ts
- do-while.ts
- while-07.ts
- aes.ts
- hof-intersection.ts
- kmp.ts
- missing-qualif.ts
- negate-00.ts
- string-accessor.ts
- transducers-00.ts
- 04-object.ts
- abs-mut.ts
- bitVector-00.ts
- bitvector-02.ts
- bitwise-00.ts
- bracketref-00.ts
- compound-assignment-operator.ts
- eq.ts
- float-00.ts
- lor-07.ts
- short-circuit.ts
- void.ts
- test-00.ts
- test-01.ts
- test-03.ts
- test-04.ts
- test-05.ts
- array-proto.ts
- proto-lookup1.ts
- proto-lookup2.ts
- proto-lookup3.ts
- proto-lookup4.ts
- proto-lookup5.ts
- proto-lookup6.ts
- proto-lookup7.ts
- proto-lookup8.ts
- 66-variadic.ts
- 67-variadic.ts
- 70-opt-args.ts
- init-01.ts
- late-init.ts
- modules.ts
- null-undef-literals.ts
- or-undef.ts
- animals.ts
- order.ts
- slowMul.ts
- splay-00.ts
- var-decl.ts
- ssa-bug-3.ts
- .gitignore
- bench.hs
- cleanup
- test.hs
- .gitattributes
- .gitignore
- .gitmodules
- .travis.yml
- LICENSE
- LICENSE.LangES
- liquid-fixpoint
- README.md
- refscript.cabal
- Setup.hs
- stack.yaml
- TODO.md
# Installation Guide
1. Get the code
git clone https://github.com/UCSD-PL/refscript
Downloads the entire project code from GitHub to your computer.
cd refscript
Moves into the project folder you just downloaded.
2. Node.js
Easy RecommendedPrerequisites
cd scripts
This project's files live in a subfolder, so move into it first.
npm install
Downloads and installs the libraries listed in package.json.
npm start
Starts the development/run server.
After running the command, open the address shown in the terminal (usually something like http://localhost:3000) in your browser.
3. Make
MediumPrerequisites
- Git Needed to download the project code from GitHub.
- Make Usually pre-installed on Linux/macOS. On Windows, install separately (e.g. via MSYS2 or WSL).
β οΈ This is a large repository, so this method may point to an internal sub-package rather than the actual core product. Check the full README as well.
cd doc/formal
This project's files live in a subfolder, so move into it first.
make
Compiles the code based on the generated build configuration to produce an executable.
If it finishes without errors, it worked. Try running the generated executable directly.
// repository documentation
Was this content helpful?
(0 ratings)