![[ICO]](/icons/blank.gif){kind=icon}
![[PARENTDIR]](/icons/back.gif){kind=icon}
![[ ]](/icons/a.gif){kind=icon}
![[ ]](/icons/layout.gif){kind=icon}
![[ ]](/icons/tex.gif){kind=icon}
![[TXT]](/icons/text.gif){kind=icon}
| Name | Last modified | Size | Description |
|---|---|---|---|---|
| Parent Directory | - | ||
| imps-2.0-manual.ps | 2012-03-27 15:38 | 1.2M | |
| undefinedness.pdf | 2012-03-27 15:38 | 1.2M | |
| panoptes.pdf | 2012-03-27 15:38 | 913K | |
| imps-1.0-manual.pdf | 2016-09-15 13:25 | 845K | |
| imps-2.0-manual.pdf | 2016-09-15 13:25 | 786K | |
| t-manual.pdf | 2012-03-27 15:38 | 741K | |
| chiron-tr.pdf | 2013-05-27 09:43 | 679K | |
| stt-with-uqe.pdf | 2015-06-14 21:48 | 656K | |
| qe-in-church.pdf | 2021-01-24 14:15 | 577K | |
| formalizing-mk.pdf | 2019-06-25 15:22 | 553K | |
| realms.pdf | 2019-08-16 14:27 | 532K | |
| monoids.pdf | 2024-11-15 10:53 | 528K | |
| exercise-solutions.pdf | 2024-04-24 16:42 | 485K | |
| hol-light-qe.pdf | 2018-08-20 13:38 | 409K | |
| andrews.pdf | 2014-06-29 07:56 | 404K | |
| syntax.pdf | 2014-06-24 13:48 | 400K | |
| seven-virtues.pdf | 2019-12-05 22:18 | 391K | |
| morphisms.pdf | 2024-02-16 14:59 | 387K | |
| qe-in-church-ss.pdf | 2017-07-23 07:59 | 359K | |
| towards-spec-sym-com..> | 2019-07-24 20:39 | 345K | |
| chiron-intro.pdf | 2012-12-28 10:09 | 345K | |
| fcl.pdf | 2020-10-25 16:42 | 339K | |
| int-inn-mathscheme-a..> | 2013-05-24 17:46 | 333K | |
| latex-for-alonzo.pdf | 2024-10-20 08:38 | 322K | |
| corrigenda.pdf | 2024-10-26 07:26 | 321K | |
| imps-overview.pdf | 2012-03-27 15:38 | 317K | |
| quote-eval.pdf | 2013-09-09 08:32 | 315K | |
| calculus.pdf | 2018-06-21 16:09 | 315K | |
| ffmm-overview.pdf | 2012-03-27 15:38 | 312K | |
| interpretations.pdf | 2012-03-27 15:38 | 307K | |
| leveraging.pdf | 2021-07-23 12:36 | 301K | |
| redex-capturing.pdf | 2020-11-27 09:49 | 290K | |
| new-proof-style-arxi..> | 2019-09-16 14:03 | 271K | |
| partial-functions.pdf | 2019-02-18 16:22 | 260K | |
| bt-proj-desc.pdf | 2018-08-20 13:32 | 258K | |
| numerical-programs.pdf | 2012-03-27 15:38 | 248K | |
| copy-on-write.pdf | 2012-03-27 15:38 | 248K | |
| cv.pdf | 2024-11-15 10:53 | 245K | |
| stmm.pdf | 2012-03-27 15:38 | 240K | |
| intertheory.pdf | 2012-03-27 15:38 | 239K | |
| csp-in-imps.pdf | 2012-03-27 15:38 | 239K | |
| overwriting-theories..> | 2012-03-27 15:38 | 239K | |
| trust-com.pdf | 2012-03-27 15:38 | 233K | |
| fcl-prelim.pdf | 2017-01-14 08:30 | 222K | |
| virtual-memory.pdf | 2012-03-27 15:38 | 221K | |
| microkernel.pdf | 2012-03-27 15:38 | 220K | |
| little-theories.pdf | 2012-03-27 15:38 | 215K | |
| trustcom-short.pdf | 2012-03-27 15:38 | 213K | |
| mkm-review.pdf | 2012-03-27 15:38 | 210K | |
| framework.pdf | 2012-03-27 15:38 | 198K | |
| trustcom-tr.pdf | 2012-03-27 15:38 | 195K | |
| pragmatics.pdf | 2012-03-27 15:38 | 193K | |
| nbg-star.pdf | 2012-03-27 15:38 | 192K | |
| transformers.pdf | 2012-03-27 15:38 | 189K | |
| rat-recon.pdf | 2012-03-27 15:38 | 184K | |
| new-proof-style.pdf | 2018-09-25 20:45 | 184K | |
| chiron-biform.pdf | 2012-03-27 15:38 | 177K | |
| esorics96.pdf | 2012-03-27 15:38 | 169K | |
| two-proofs.pdf | 2012-03-27 15:38 | 169K | |
| niss96.pdf | 2012-03-27 15:38 | 165K | |
| hlt.pdf | 2012-03-27 15:38 | 158K | |
| scss-2014-ext-abs.pdf | 2023-01-18 12:24 | 157K | |
| fmfm.pdf | 2022-05-10 21:46 | 156K | |
| mech-trad-approach.pdf | 2012-03-27 15:38 | 145K | |
| mathscheme-library.pdf | 2012-03-27 15:38 | 145K | |
| chiron-notation.pdf | 2012-03-27 15:38 | 136K | |
| cade-13-sys-desc.pdf | 2012-03-27 15:38 | 134K | |
| cade-11-sys-desc.pdf | 2012-03-27 15:38 | 121K | |
| iml-proposal.pdf | 2012-03-27 15:38 | 118K | |
| MTP-261.pdf | 2012-03-27 15:38 | 117K | |
| new-field.pdf | 2012-03-27 15:38 | 116K | |
| bestt.pdf | 2012-03-27 15:38 | 116K | |
| rec-def.pdf | 2012-03-27 15:38 | 108K | |
| perspect-switching.pdf | 2012-03-27 15:38 | 93K | |
| sttwu-completeness.pdf | 2012-03-27 15:38 | 93K | |
| notation.pdf | 2012-03-27 15:38 | 60K | |
| cicm-2011-proj-desc.pdf | 2012-03-27 15:38 | 58K | |
| imps-bibliography.pdf | 2012-03-27 15:38 | 55K | |
| paper-tips.pdf | 2012-03-27 15:38 | 49K | |
| The_Great_Truth_abou..> | 2019-08-20 07:52 | 48K | |
| talk-tips.pdf | 2012-03-27 15:38 | 39K | |
| alonzo-notation.tex | 2024-11-19 11:02 | 21K | |
| imps-bibliography.bib | 2012-03-27 15:38 | 17K | |
| imps-bibliography.html | 2012-03-27 15:38 | 11K | |
| major-imps-papers.html | 2012-03-27 15:38 | 7.6K | |
| tetrapod-survey-abs.txt | 2020-02-17 09:34 | 2.4K | |
| wmf-thesis-abs.txt | 2012-03-27 15:38 | 2.0K | |
| suggestions.html | 2016-05-09 13:03 | 1.8K | |
| fcl-abs.txt | 2018-06-14 11:25 | 1.6K | |
| quote-eval-abs.txt | 2013-04-23 15:57 | 1.6K | |
| chiron-tr-abs.txt | 2013-05-27 09:43 | 1.5K | |
| fcl-prelim-abs.txt | 2017-01-14 08:30 | 1.5K | |
| fmfm-abs.txt | 2021-07-23 12:36 | 1.4K | |
| stt-with-uqe-abs.txt | 2017-07-23 08:07 | 1.3K | |
| better-style-abs.txt | 2018-03-07 13:20 | 1.3K | |
| keys-to-success.html | 2016-05-09 13:03 | 1.3K | |
| syntax-abs.txt | 2013-07-12 09:19 | 1.3K | |
| ffmm-overview-abs.txt | 2012-03-27 15:38 | 1.2K | |
| nbg-star-abs.txt | 2012-03-27 15:38 | 1.2K | |
| ffmm-abs.txt | 2012-03-27 15:38 | 1.2K | |
| redex-capturing-abs.txt | 2012-03-27 15:38 | 1.2K | |
| k-provability-abs.txt | 2012-03-27 15:38 | 1.2K | |
| PATE-2007-abs.txt | 2012-03-27 15:38 | 1.2K | |
| monoids-abs.txt | 2023-12-09 14:55 | 1.1K | |
| formalizing-mk-abs.txt | 2017-04-10 08:03 | 1.1K | |
| chiron-biform-abs.txt | 2012-03-27 15:38 | 1.1K | |
| partial-functions-ab..> | 2012-03-27 15:38 | 1.0K | |
| realms-abs.txt | 2014-06-02 21:03 | 1.0K | |
| cicm-2011-proj-desc-..> | 2012-03-27 15:38 | 1.0K | |
| imps-overview-abs.txt | 2012-03-27 15:38 | 1.0K | |
| bt-proj-desc-abs.txt | 2018-06-12 11:42 | 1.0K | |
| calculus-abs.txt | 2019-04-08 18:17 | 1.0K | |
| 2nd-ord-monadic-abs.txt | 2012-03-27 15:38 | 1.0K | |
| new-proof-style-for-..> | 2018-12-07 14:27 | 1.0K | |
| kreisel-abs.txt | 2012-03-27 15:38 | 1.0K | |
| rat-recon-abs.txt | 2012-03-27 15:38 | 1.0K | |
| trustcom-tr-abs.txt | 2012-03-27 15:38 | 1.0K | |
| esorics96-abs.txt | 2012-03-27 15:38 | 969 | |
| stmm-abs.txt | 2012-03-27 15:38 | 967 | |
| y-correct-abs.txt | 2012-03-27 15:38 | 955 | |
| trustcom-short-abs.txt | 2012-03-27 15:38 | 948 | |
| andrews-abs.txt | 2016-05-23 09:51 | 948 | |
| big-math-abs.txt | 2019-11-12 11:37 | 940 | |
| leveraging-abs.txt | 2021-07-23 12:36 | 921 | |
| contexts-abs.txt | 2012-03-27 15:38 | 911 | |
| discipline-abs.txt | 2012-03-27 15:38 | 878 | |
| hol-light-qe-abs.txt | 2018-05-19 08:42 | 858 | |
| mtps-abs.txt | 2012-03-27 15:38 | 823 | |
| trust-com-abs.txt | 2012-03-27 15:38 | 816 | |
| pf-star-abs.txt | 2012-03-27 15:38 | 800 | |
| simple-steps-abs.txt | 2012-03-27 15:38 | 790 | |
| 2nd-ord-unification-..> | 2012-03-27 15:38 | 788 | |
| morphisms-abs.txt | 2017-03-07 20:28 | 779 | |
| qe-in-church-abs.txt | 2023-02-11 08:18 | 765 | |
| panoptes-abs.txt | 2012-03-27 15:38 | 759 | |
| interpretations-abs.txt | 2012-03-27 15:38 | 731 | |
| qe-in-church-ss-abs.txt | 2016-05-23 12:39 | 730 | |
| new-field-abs.txt | 2019-04-23 10:35 | 729 | |
| towards-spec-sym-com..> | 2019-04-07 11:50 | 725 | |
| intertheory-abs.txt | 2012-03-27 15:38 | 721 | |
| pf-abs.txt | 2012-03-27 15:38 | 717 | |
| mkm-review-abs.txt | 2012-03-27 15:38 | 715 | |
| transformers-abs.txt | 2012-03-27 15:38 | 710 | |
| k-prov-Gentzen-abs.txt | 2012-03-27 15:38 | 677 | |
| iml-paper-abs.txt | 2012-03-27 15:38 | 666 | |
| seven-virtues-abs.txt | 2012-03-27 15:38 | 662 | |
| curry-chip-abs.txt | 2012-03-27 15:38 | 662 | |
| microkernel-abs.txt | 2012-03-27 15:38 | 659 | |
| niss96-abs.txt | 2012-03-27 15:38 | 648 | |
| new-proof-style-abs.txt | 2018-06-11 11:56 | 643 | |
| framework-abs.txt | 2012-03-27 15:38 | 643 | |
| overwriting-theories..> | 2012-03-27 15:38 | 622 | |
| chiron-intro-abs.txt | 2012-03-27 15:38 | 594 | |
| rec-def-abs.txt | 2012-03-27 15:38 | 554 | |
| numerical-programs-a..> | 2012-03-27 15:38 | 547 | |
| mkm-in-ekm-abs.txt | 2012-03-27 15:38 | 507 | |
| mech-trad-approach-a..> | 2012-03-27 15:38 | 497 | |
| mathscheme-library-a..> | 2012-03-27 15:38 | 494 | |
| little-theories-abs.txt | 2012-03-27 15:38 | 490 | |
| hlt-abs.txt | 2012-03-27 15:38 | 466 | |
| bestt-abs.txt | 2012-03-27 15:38 | 371 | |
| sttwu-completeness-a..> | 2012-03-27 15:38 | 337 | |
| imps-17-provers-abs.txt | 2012-03-27 15:38 | 259 | |
| latex-for-alonzo-abs..> | 2023-07-11 12:04 | 238 | |
| pragmatics-abs.txt | 2012-03-27 15:38 | 220 | |