A FORTRAN-90 low-energy electron diffraction program (LEED90 v1.1)

We describe a FORTRAN-90 program to compute low-energy electron diffraction I(V) curves. Plane-waves and layer doubling are used to compute the inter-layer multiple-scattering, while the intra-layer multiple-scattering is computed in the standard way expanding the wavefield on a basis of spherical waves. The program is kept as general as possible, in order to allow testing different parts of multiple-scattering calculations. In particular, it can handle non-diagonal t-matrices describing the scattering of non-spherical potentials, anisotropic vibrations, anharmonicity, etc. The program does not use old FORTRAN flavours, and has been written keeping in mind the advantage for parallelism brought forward by FORTRAN-90.

Computer Theorem Proving and HoTT

Theorem-proving is a one-player game. The history of computer programs being the players goes back to 1956 and the ‘LT’ LOGIC THEORY MACHINE of Newell, Shaw and Simon. In game-playing terms, the ‘initial position’ is the core set of axioms chosen for the particular logic and the ‘moves’ are the rules of inference. Now, the Univalent Foundations Program at IAS Princeton and the resulting ‘HoTT’ book on Homotopy Type Theory have demonstrated the success of a new kind of experimental mathematics using computer theorem proving.