CSE-490 Logic in Computer Science - Software

[ Home | Schedule | Assignments | Software | Resources | Students ] gla@postech Sungwoo Park


Standard ML of New Jersey (Required)

  • For the lectures and assignments, we will use Standard ML of New Jersey (commonly abbreviated as SML/NJ). Install the latest working version 110.58 from here.
  • For Cygwin users, be sure to read CYGWININSTALL to properly install the software. If sml complains that it cannot find the runtime system (for example /usr/bin/smlnj/bin/.run/run.x86-win32), try setting the environment variable SMLNJ_CYGWIN_RUNTIME:

    setenv SMLNJ_CYGWIN_RUNTIME 1 (in csh)

  • If you have any trouble with installing the software on your system, please email the teaching staff.

The Coq proof assistant (Required)

  • We will use the Coq proof assistant for writing proofs in several assignments.
  • Please download and install the current version Coq 8.0 from the home page of the Coq project.

AFS client (Required)

  • You need to have some way to access the Hemos AFS (Andrew File System). Check out the FAQ section of the Hemos webpage for a brief introduction to the AFS(search "AFS User Guide").
  • If you want to mount the AFS on your local machine, visit http://www.openafs.org and install the client software. Use postech.ac.kr as the cell name.

Latex (Required)

  • You are required to typeset your answers to written assignments, and we strongly recommend Latex for typesetting your answers. The Latex commands for math formulae were adoptedy by 아래아한글 (HWP), so they should not be completely strange to you.
  • For Windows, you can use MiKTex whose basic system (~32MB) contains all necessary packages and software. (The complete system takes about 380MB of disk space.) Install it and change the PATH variable to include the directory containing executable files (e.g., C:\texmf\miktex\bin; under a typical installation). To produce a PS or PDF file, follow these steps:
    • Edit a tex file using your favorite editor (e.g., a.tex).
    • Compile it using the program latex (e.g., latex a.tex).
    • The compilation produces a dvi file (e.g., a.dvi). You can view the result using the program yap.
    • Convert the dvi file to a PS file using the program dvips ((e.g., dvips a.dvi).
    • Alternatively you can produce a PDF file using the program pdflatex ((e.g., pdflatex a.tex).
    • To view PS files, you want to install ghostscript and ghostview.
    • To view PDF files, you want to install Acrobat Reader.
  • On Cygwin, you can select the TeTex package during the installation procedure. On Linux, the Latex software is included in the default installation. Be sure to set the environment variable path properly.
    • You can use xdvi to view your dvi files. (There is no yap on Linux and Cygwin.)
    • Use the ghostview program gv to view PS files.
    • You can use Acrobat Reader or xpdf to view PDF files.

[ Home | Schedule | Assignments | Software | Resources | Students ] gla@postech Sungwoo Park