<thomashartm...@gmail.com> wrote:
> Todd and I rescheduled to tomorrow at noon. If there's anyone in the
> L.A. area that wants to stop by, you're welcome. Otherwise, hope to
> see you on skype.

> Please let me know if you can make this time so I know who to call :)

> On Sat, Jul 21, 2012 at 10:20 PM, Thomas Hartman
> <thomashartm...@gmail.com> wrote:
>> Yes, let's push back a week.

>> On Jul 21, 2012 7:38 PM, "Todd Rockhold" <todd_rockh...@yahoo.com> wrote:

>>> Hmmm ... looks like no meeting.  I can't get my computer audio going for a
>>> Google+ hangout type thing.  And it seems that something unanticipated has
>>> come up for Tom.  I believe Rob is in New York and probably busy with
>>> something else.

>>> How about next Saturday, the 28th, at 7 PM?

>>> --- On Sun, 7/15/12, Thomas Hartman <tho...@marketpsychdata.com> wrote:

>>> > From: Thomas Hartman <tho...@marketpsychdata.com>
>>> > Subject: Re: [socalfp] Re: is this how our children will learn math? Re:
>>> > Coq reading group
>>> > To: socalfp@googlegroups.com
>>> > Cc: "Todd Rockhold" <todd_rockh...@yahoo.com>, "Mike Vanier"
>>> > <mvanie...@gmail.com>
>>> > Date: Sunday, July 15, 2012, 10:57 PM
>>> > So, we have 3 yays for Saturday 7pm.
>>> > I say let's do it.

>>> > Agreed?

>>> > On Sun, Jul 15, 2012 at 10:45 PM, Rob Zinkov <rzin...@gmail.com>
>>> > wrote:
>>> > > I'll see if I can remote in.

>>> > > On Jul 16, 2012 1:36 AM, "Thomas Hartman" <tho...@marketpsychdata.com>
>>> > > wrote:

>>> > >> OK, we'll try to keep the flame burning in the
>>> > meantime.

>>> > >> On Sun, Jul 15, 2012 at 10:32 PM, Michael Vanier
>>> > <mvanie...@gmail.com>
>>> > >> wrote:
>>> > >> > Guys,

>>> > >> > Really sorry to have missed it!  I had a
>>> > hellish weekend with lots of
>>> > >> > boring
>>> > >> > social stuff I couldn't get out of.  It's
>>> > going to be tough for me until
>>> > >> > this course is over (ends in late July), but
>>> > after that I'll have about
>>> > >> > two
>>> > >> > months free, so I'd like to get some meetings
>>> > in.

>>> > >> > Mike

>>> > >> > On 7/15/12 10:21 PM, Thomas Hartman wrote:

>>> > >> >> Update: Todd and I had a phone meeting
>>> > where we didn't work on
>>> > >> >> software foundations but just discussed
>>> > potential directions a
>>> > >> >> dependent types / formal methods study
>>> > group could move in.

>>> > >> >> We agree that it would be a good idea to
>>> > confinue with pierce's SF, so
>>> > >> >> no change there.

>>> > >> >> Passing on from that we discussed

>>> > >> >> Homotopy Type Theory / Foundations of
>>> > mathemactics:
>>> > >> >>    We touched briefly on the
>>> > news that HOTT group will likely create a
>>> > >> >> new proof assistant rather than proceed
>>> > with their program using coq

>>> > >> >> https://groups.google.com/forum/?fromgroups#!topic/HomotopyTypeTheory...
>>> > >> >>    We also indulged in some
>>> > speculation about "non acadenic" use of
>>> > >> >> HOTT/and I guess higher dimensional
>>> > topology in general. Two ideas
>>> > >> >> emerged
>>> > >> >>      -- graphics engines /
>>> > video games
>>> > >> >>      -- dimensional
>>> > reduction in machine learning
>>> > >> >>      We might be on thin
>>> > ice here, so caveat emptor.

>>> > >> >> I indicated interest in "real world coq /
>>> > dependent types / formal
>>> > >> >> methods."
>>> > >> >>    So, basically learning more
>>> > about
>>> > >> >>      -- actual uses of
>>> > coq/dependent types other than proving math
>>> > >> >> theorems. Examples include
>>> > >> >>        -- verification
>>> > of l4 microkernel

>>> >    -- compcert

>>> >    -- check the galois blog for more
>>> > examples

>>> >    suggested activity -- learn more about
>>> > these "real world"
>>> > >> >> projects and try to get a feel for
>>> > "industrial verification" type
>>> > >> >> work.
>>> > >> >>          Maybe
>>> > more tractable:

>>> >    -- http://logitext.mit.edu/main
>>> > <borderline mathy, but it
>>> > >> >> includes getting the UrWeb dependently
>>> > typed web framework to play
>>> > >> >> nicely with coq, which is pretty cool>

>>> >    Suggested group hacktivity: install and
>>> > run logitext locally,
>>> > >> >> to gain familiarity with these tools in a
>>> > semi-production setting
>>> > >> >>      -- developing an
>>> > intuition for "nails that fit the hammer of
>>> > >> >> formal methods" in other respects

>>> > >> >> We also talked a bit about
>>> > epigram/epigram2.
>>> > >> >> I really enjoyed the epigram papers, and
>>> > it seems to be a really
>>> > >> >> creative direction to take in terms of
>>> > bringing dependen types to the
>>> > >> >> "real world."
>>> > >> >> The project seems to be hybernated,
>>> > unfortunately.
>>> > >> >> Suggested hacktivity: Install
>>> > she/epigram/epigram2, do some
>>> > >> >> exploratory programming, do some
>>> > cheerleading to try to get project
>>> > >> >> unhybernated. OK, maybe this is a long
>>> > shot.

>>> > >> >> Finally, we suggested meeting next
>>> > saturday (7/21) at 7pm for our next
>>> > >> >> coqathon (or better, "coqus?") where we
>>> > would cover chapter 2 of SF.
>>> > >> >> This would be most likely a remote
>>> > meetup.

>>> > >> >> What do you think, Mike Vanier/others?

>>> > >> >> Thomas.

>>> > >> >> On Tue, Jul 10, 2012 at 4:28 PM, Thomas
>>> > Hartman
>>> > >> >> <tho...@marketpsychdata.com>
>>> > wrote:

>>> > >> >>> Sunday 7pm is okay too.

>>> > >> >>> On Tue, Jul 10, 2012 at 4:05 PM, Todd
>>> > Rockhold
>>> > >> >>> <todd_rockh...@yahoo.com>
>>> > >> >>> wrote:

>>> > >> >>>>   7 PM Saturday
>>> > doesn't work for me,  but if it does for everyone
>>> > >> >>>> else,
>>> > >> >>>> maybe
>>> > >> >>>> that's that.

>>> > >> >>>> Any time Sunday would work for
>>> > me.

>>> > >> >>>> ----- Original Message ----
>>> > >> >>>> From: Thomas Hartman <tho...@marketpsychdata.com>
>>> > >> >>>> To: socalfp@googlegroups.com
>>> > >> >>>> Cc: Rob Zinkov <rzin...@gmail.com>;
>>> > Mike Klein
>>> > >> >>>> <javasucks...@gmail.com>;
>>> > >> >>>> "todd_rockh...@yahoo.com"
>>> > <todd_rockh...@yahoo.com>;
>>> > Mike Vanier
>>> > >> >>>> <mvanie...@gmail.com>
>>> > >> >>>> Sent: Tue, July 10, 2012 12:02:24
>>> > PM
>>> > >> >>>> Subject: Re: [socalfp] Re: is this
>>> > how our children will learn math?
>>> > >> >>>> Re:
>>> > >> >>>> Coq
>>> > >> >>>> reading group

>>> > >> >>>> How about Saturday at 7pm?

>>> > >> >>>> On Sun, Jul 8, 2012 at 8:03 PM,
>>> > Michael Vanier <mvanie...@gmail.com>
>>> > >> >>>> wrote:

>>> > >> >>>>> I'm definitely
>>> > interested.  I'm teaching a summer course for the
>>> > >> >>>>> next
>>> > >> >>>>> three
>>> > >> >>>>> weeks, so I can only meet on
>>> > the weekends (preferably late Saturday
>>> > >> >>>>> or
>>> > >> >>>>> Sunday).

>>> > >> >>>>> Mike

>>> > >> >>>>> On 7/8/12 12:52 PM, Thomas
>>> > Hartman wrote:

>>> > >> >>>>>> http://perso.ens-lyon.fr/jeanmarie.madiot/coq100/

>>> > >> >>>>>> 48 theorems left to
>>> > formalize.

>>> > >> >>>>>> Anyone want to meet up?

>>> > >> >>>>>> On Sat, Jan 7, 2012 at
>>> > 12:04 PM, Thomas Hartman
>>> > >> >>>>>> <tho...@marketpsychdata.com>
>>> > wrote:

>>> > >> >>>>>>> 10am works for me, and
>>> > changed subject to contain correct time.
>>> > >> >>>>>>> Whoops.

>>> > >> >>>>>>> On Jan 7, 2012 10:23
>>> > AM, "Rob Zinkov" <rzin...@gmail.com>
>>> > wrote:

>>> > >> >>>>>>>> 10am works for me

>>> > >> >>>>>>>> On Jan 7, 2012
>>> > 1:08 PM, "Michael Vanier" <mvanie...@gmail.com>
>>> > >> >>>>>>>> wrote:

>>> > >> >>>>>>>>> I can't do 1
>>> > PM at all.  I can do 10 AM - 1 PM, or I'm free the
>>> > >> >>>>>>>>> entire
>>> > >> >>>>>>>>> next weekend.

>>> > >> >>>>>>>>> BTW Thomas and
>>> > I were talking about iteratees, and Mike Snoyman
>>> > >> >>>>>>>>> wrote
>>> > >> >>>>>>>>> this very nice
>>> > tutorial on them:

>>> > >> >>>>>>>>> http://www.yesodweb.com/book/enumerator

>>> > >> >>>>>>>>> Mike

>>> > >> >>>>>>>>> On 1/7/12 9:35
>>> > AM, Thomas Hartman wrote:

>>> > >> >>>>>>>>>> Is this
>>> > time ok?

>>> > >> >>>>>>>>>> Todd could
>>> > you cc your friend in hawaii? I forgot his name.

>>> > >> >>>>>>>>>> ----------
>>> > Forwarded message ----------
>>> > >> >>>>>>>>>> From:
>>> > "Michael Vanier" <mvanie...@gmail.com

>>> > <mailto:mvanie...@gmail.com>>
>>> > >> >>>>>>>>>> Date: Jan
>>> > 6, 2012 11:09 PM
>>> > >> >>>>>>>>>> Subject:
>>> > Re: Coq meetup 2pm next sat (tomorrow plus one week)
>>> > >> >>>>>>>>>> To:
>>> > "Thomas Hartman" <tho...@marketpsychdata.com

>>> > <mailto:tho...@marketpsychdata.com>>

>>> > >> >>>>>>>>>> On 1/6/12
>>> > 10:44 PM, Thomas Hartman wrote:

>>> >     I can't do afternoon that Saturday. How about
>>> > morning,
>>> > >> >>>>>>>>>> like
>>> > >> >>>>>>>>>> 10am?

>>> >     Or Sunday 2pm?

>>> >     On Jan 6, 2012 10:18 PM, "Michael Vanier"
>>> > >> >>>>>>>>>> <mvanie...@gmail.com

>>> >     <mailto:mvanie...@gmail.com>
>>> > <mailto:mvanie...@gmail.com

>>> >     <mailto:mvanie...@gmail.com>>>
>>> > wrote:

>>> >        Thomas,

>>> >        My phone just died --
>>> > sorry.  Anyway, we should plan
>>> > >> >>>>>>>>>> for 2
>>> > >> >>>>>>>>>> PM
>>> > >> >>>>>>>>>> next

>>> >        Saturday unless otherwise
>>> > indicated (i.e. unless my
>>> > >> >>>>>>>>>> wife
>>> > >> >>>>>>>>>> has

>>> >        already scheduled something,
>>> > which I'll check).  Thanks
>>> > >> >>>>>>>>>> for

>>> >     calling!

>>> >        Mike

>>> > >> >>>>>>>>>> Morning at
>>> > 10 AM works for me, with the caveat that I have to
>>> > >> >>>>>>>>>> leave at
>>> > >> >>>>>>>>>> 1
>>> > >> >>>>>>>>>> PM.

>>> > >> >>>>>>>>>> Mike

>>> > >> >>>>> --
>>> > >> >>>>> Southern California Functional
>>> > Programmers:
>>> > >> >>>>> socalfp@googlegroups.com.
>>> > >> >>>>> Policies: http://groups.google.com/group/socalfp/web/policies
>>> > >> >>>>> Unsubscribe: socalfp-unsubscribe@googlegroups.com
>>> > >> >>>>> Other Options: http://groups.google.com/group/socalfp

>>> > >> >>>> --
>>> > >> >>>> --
>>> > >> >>>> _____________________
>>> > >> >>>> Thomas Hartman
>>> > >> >>>> MarketPsych LLC
>>> > >> >>>> MarketPsy Capital  LLC
>>> > >> >>>> 2400 Broadway, Suite 220
>>> > >> >>>> Santa Monica, CA, USA
>>> > >> >>>> Tel:  +1.310.573.8523
>>> > >> >>>> ______________________

>>> > >> >>>> This e-mail message and any
>>> > attachments may contain information that
>>> > >> >>>> is confidential, proprietary or
>>> > privileged, and is for the named
>>> > >> >>>> person’s use only.  No
>>> > confidentiality or privilege is waived or lost
>>> > >> >>>> by any mistransmission.  If
>>> > you are not the intended recipient or
>>> > >> >>>> agent responsible for delivering
>>> > it to the intended recipient, you
>>> > >> >>>> are
>>> > >> >>>> hereby notified that any
>>> > dissemination, distribution, copying or
>>> > >> >>>> other
>>> > >> >>>> use of this message or its
>>> > attachments is strictly prohibited.  If
>>> > >> >>>> you
>>> > >> >>>> have received this message in
>>> > error, please notify us immediately and
>>> > >> >>>> destroy all copies of this message
>>> > and attachments without disclosing
>>> > >> >>>> the contents to anyone.
>>> > Neither this message nor any information
>>> > >> >>>> included herein constitute an
>>> > offer to sell or the solicitation of an
>>> > >> >>>> offer to buy any securities or
>>> > investment product, or legal, tax,
>>> > >> >>>> accounting, or investment advice.

>>> > >> >>>> --
>>> > >> >>>> Southern California Functional
>>> > Programmers: socalfp@googlegroups.com.
>>> > >> >>>> Policies: http://groups.google.com/group/socalfp/web/policies
>>> > >> >>>> Unsubscribe: socalfp-unsubscribe@googlegroups.com
>>> > >> >>>> Other Options: http://groups.google.com/group/socalfp

>>> > >> >>>> --
>>> > >> >>>> Southern California Functional
>>> > Programmers: socalfp@googlegroups.com.
>>> > >> >>>> Policies: http://groups.google.com/group/socalfp/web/policies
>>> > >> >>>> Unsubscribe: socalfp-unsubscribe@googlegroups.com
>>> > >> >>>> Other Options: http://groups.google.com/group/socalfp

>>> > >> >>> --
>>> > >> >>> --
>>> > >> >>> _____________________
>>> > >> >>> Thomas Hartman
>>> > >> >>> MarketPsych LLC
>>> > >> >>> MarketPsy Capital  LLC
>>> > >> >>> 2400 Broadway, Suite 220
>>> > >> >>> Santa Monica, CA, USA
>>> > >> >>> Tel:  +1.310.573.8523
>>> > >> >>> ______________________

>>> > >> >>> This e-mail message and any
>>> > attachments may contain information that
>>> > >> >>> is confidential, proprietary or
>>> > privileged, and is for the named
>>> > >> >>> person’s use only.  No
>>> > confidentiality or privilege is waived or lost
>>> > >> >>> by any mistransmission.  If you
>>> > are not the intended recipient or
>>> > >> >>> agent responsible for delivering it to
>>> > the intended recipient, you are
>>> > >> >>> hereby notified that any
>>> > dissemination, distribution, copying or other
>>> > >> >>> use of this message or its attachments
>>> > is strictly prohibited.  If you
>>> > >> >>> have received this message in error,
>>> > please notify us immediately and
>>> > >> >>> destroy all copies of this message and
>>> > attachments without disclosing
>>> > >> >>> the contents to anyone.  Neither
>>> > this message nor any information
>>> > >> >>> included herein constitute an offer to
>>> > sell or the solicitation of an
>>> > >> >>> offer to buy any securities or
>>> > investment product, or legal, tax,
>>> > >> >>> accounting, or investment advice.

>>> > >> > --
>>> > >> > Southern California Functional Programmers:
>>> > >> > socalfp@googlegroups.com.
>>> > >> > Policies: http://groups.google.com/group/socalfp/web/policies
>>> > >> > Unsubscribe: socalfp-unsubscribe@googlegroups.com
>>> > >> > Other Options: http://groups.google.com/group/socalfp

>>> > >> --
>>> > >> --
>>> > >> _____________________
>>> > >> Thomas Hartman
>>> > >> MarketPsych LLC
>>> > >> MarketPsy Capital  LLC
>>> > >> 2400 Broadway, Suite 220
>>> > >> Santa Monica, CA, USA
>>> > >> Tel:  +1.310.573.8523
>>> > >> ______________________

>>> > >> This e-mail message and any attachments may contain
>>> > information that
>>> > >> is confidential, proprietary or privileged, and is
>>> > for the named
>>> > >> person’s use only.  No confidentiality or
>>> > privilege is waived or lost
>>> > >> by any mistransmission.  If you are not the
>>> > intended recipient or
>>> > >> agent responsible for delivering it to the intended
>>> > recipient, you are
>>> > >> hereby notified that any dissemination,
>>> > distribution, copying or other
>>> > >> use of this message or its attachments is strictly
>>> > prohibited.  If you
>>> > >> have received this message in error, please notify
>>> > us immediately and
>>> > >> destroy all copies of this message and attachments
>>> > without disclosing
>>> > >> the contents to anyone.  Neither this message
>>> > nor any information
>>> > >> included herein constitute an offer to sell or the
>>> > solicitation of an
>>> > >> offer to buy any securities or investment product,
>>> > or legal, tax,
>>> > >> accounting, or investment advice.

>>> > >> --
>>> > >> Southern California Functional Programmers: socalfp@googlegroups.com.
>>> > >> Policies: http://groups.google.com/group/socalfp/web/policies
>>> > >> Unsubscribe: socalfp-unsubscribe@googlegroups.com
>>> > >> Other Options: http://groups.google.com/group/socalfp

>>> > > --
>>> > > Southern California Functional Programmers: socalfp@googlegroups.com.
>>> > > Policies: http://groups.google.com/group/socalfp/web/policies
>>> > > Unsubscribe: socalfp-unsubscribe@googlegroups.com
>>> > > Other Options: http://groups.google.com/group/socalfp

>>> > --
>>> > --
>>> > _____________________
>>> > Thomas Hartman
>>> > MarketPsych LLC
>>> > MarketPsy Capital  LLC
>>> > 2400 Broadway, Suite 220
>>> > Santa Monica, CA, USA
>>> > Tel:  +1.310.573.8523
>>> > ______________________

>>> > This e-mail message and any attachments may contain
>>> > information that
>>> > is confidential, proprietary or privileged, and is for the
>>> > named
>>> > person’s use only.  No confidentiality or privilege
>>> > is waived or lost
>>> > by any mistransmission.  If you are not the intended
>>> > recipient or
>>> > agent responsible for delivering it to the intended
>>> > recipient, you are
>>> > hereby notified that any dissemination, distribution,
>>> > copying or other
>>> > use of this message or its attachments is strictly
>>> > prohibited.  If you
>>> > have received this message in error, please notify us
>>> > immediately and
>>> > destroy all copies of this message and attachments without
>>> > disclosing
>>> > the contents to anyone.  Neither this message nor any
>>> > information
>>> > included herein constitute an offer to sell or the
>>> > solicitation of an
>>> > offer to buy any securities or investment product, or legal,
>>> > tax,
>>> > accounting, or investment advice.

>>> > --
>>> > Southern California Functional Programmers: socalfp@googlegroups.com.
>>> > Policies: http://groups.google.com/group/socalfp/web/policies
>>> > Unsubscribe: socalfp-unsubscribe@googlegroups.com
>>> > Other Options: http://groups.google.com/group/socalfp

>>> --
>>> Southern California Functional Programmers: socalfp@googlegroups.com.
>>> Policies: http://groups.google.com/group/socalfp/web/policies
>>> Unsubscribe: socalfp-unsubscribe@googlegroups.com
>>> Other Options: http://groups.google.com/group/socalfp