|Table of Contents|
- Homeworks may require use of the course software, or a write-up as a PDF.
- Machine-checked assignments must be programmed/proved using the course software and submitted via Gradescope on the due date.
- Written parts of the assignments must be typeset and submitted in PDF via Gradescope on the due date.
- For typesetting deductions in LaTeX, we use bussproofs.sty
but you may prefer other LaTeX packages.
[bussproofs.sty | example | proof.sty | example | mathpartir.sty | example]
Assignment ScheduleThe Assignment Schedule is tentative!
For this course we continue to use Standard ML of New Jersey (SML/NJ) that you are familiar with from 15-150 Functional Programming. If you are a masters student and have not taken 15-150 before, you are expected to have acquired a background in functional programming and pick up sufficient proficiency in SML along the way.
Run the SML/NJ compiler, e.g., as
smlnj -m sources.cm[SML/NJ | Learning SML | SML base library]
For this course we are using GNU Prolog.
The Andrew Linux cluster installation of GNU Prolog on
linux.andrew.cmu.edu can be run either by running the script:
/afs/andrew/course/15/317/bin/gprologor by adding the directory
/afs/andrew/course/15/317/binto your PATH and running
gprolog. You can also download a distribution, e.g., from the GNU Prolog web site or directly from your operating system and install it on your own machine.
Most installations of vim and emacs have editing modes for Prolog code, but the default is to treat
.pl files as Perl code.
Switching files to Prolog mode works as follows:
enables the Prolog menus and
^C ^Lconsults the current file with Prolog. If that does not work, install prolog mode for emacs and add prolog.el:
; M-x customize Prolog program name (load "~/.emacs.d/lisp/prolog.el") (autoload 'run-prolog "prolog" "Start Prolog interpreter." t) (autoload 'prolog-mode "prolog" "Major mode for Prolog." t) (autoload 'mercury-mode "prolog" "Major mode for Mercury." t) (setq prolog-system 'gnu) (add-to-list 'auto-mode-alist '("\\.pl\\'" . prolog-mode)) (setq prolog-electric-if-then-else-flag t) (setq prolog-align-small-comments-flag nil) ; don't indent % comments
C-h mhelp on key bindings
C-c C-fconsult file to load it
- Emacs: EdiProlog mode for emacs with SWI Prolog and Scryer Prolog, add ediprolog.el:
(F10 consults the point. C-u C-u F10 reloads file consulting the point.)
; EdiProlog M-x customize-group ediprolog (require 'ediprolog "~/.emacs.d/lisp/ediprolog.el") (global-set-key [f10] 'ediprolog-dwim) (add-to-list 'auto-mode-alist '("\\.pl\\'" . prolog-mode))