*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Where to learn about HOL vs FOL?*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Fri, 01 Feb 2013 08:22:53 -0600*In-reply-to*: <op.wrsjuyeuule2fv@cardamome>*References*: <op.wrrj47uzule2fv@cardamome> <510A79F0.9050308@gmx.com> <CAAPnxw2g6Di9MEmQgyqhf_+NBW5HLrVAPi2JVxohcFLTqWe1dA@mail.gmail.com> <op.wrsjuyeuule2fv@cardamome>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

On 1/31/2013 1:46 PM, Yannick Duchêne (Hibou57) wrote:

Seems available on‑line; here is a link for the paper you suggest: http://www.sciencedirect.com/science/article/pii/S157086830700081X# (the page also has a link at the top, for a PDF version)

http://imps.mcmaster.ca/doc/seven-virtues.pdf http://imps.mcmaster.ca/doc/

https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus

https://en.wikipedia.org/wiki/Type_theory#Theory_of_simple_types

http://hol.sourceforge.net/documentation.html

simply-typed : (adj) Relating to type systems that are relatively simple and are not, for example, dependently-typed. There is considerable variation in the precise intended meaning of "simply-typed" in contemporary usage: in some usages polymorphism is not a disqualifying factor, in other usages polymorphism is only a disqualifying factor if it caters for the quantification of type variables, and in other usages still any form of polymorphism is a disqualifying factor. To avoid confusion, the usage of this term is avoided in HOL Zero, its documentation and elsewhere in this glossary.

Still looking at Gottfried's list.

Regards, GB http://www.phil.cmu.edu/~avigad/formal/ http://www.andrew.cmu.edu/user/avigad/isabelle/ http://www4.in.tum.de/~ballarin/belgrade08-tut/ http://cl-informatik.uibk.ac.at/teaching/ss08/atp/schedule.php http://isabelle.in.tum.de/coursematerial/IJCAR04/ http://archiv.infsec.ethz.ch/education/permanent/csmr.html http://isabelle.in.tum.de/exercises/ http://www.irisa.fr/celtique/genet/ACF/ http://dream.inf.ed.ac.uk/projects/isabelle/ http://isabelle.in.tum.de/coursematerial/PSV2009-1/ http://www21.in.tum.de/teaching/logik/SS12/ http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1011/ http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1112/ http://www.cs.colorado.edu/~siek/7000/spring07/ http://ecee.colorado.edu/~siek/ecen3703/spring10/ECEN_3703.html http://cl-informatik.uibk.ac.at/teaching/ss11/eve/content.php http://www.lri.fr/~wenzel/Isar2010-Orsay/ http://www.lri.fr/~wenzel/Isabelle2011-Paris/ http://www.lri.fr/~wenzel/Isabelle_Orsay_2012/ http://www.lri.fr/~wenzel/Isabelle_Orleans_2012/

- Previous by Date: Re: [isabelle] Initialisation of session and nodes: What's changed?
- Next by Date: Re: [isabelle] New error messages in Isabelle 2013
- Previous by Thread: Re: [isabelle] Where to learn about HOL vs FOL?
- Next by Thread: Re: [isabelle] Using ISABELLE_BUILD_OPTIONS in Isabelle 2013
- Cl-isabelle-users February 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list