byu-cs-430-winter-2013

Contact owners and managers

1–30 of 53

0 selected

5/2/13

I got these two good comments: "I would suggest having a more regular evaluation of where

unread,

I got these two good comments: "I would suggest having a more regular evaluation of where

5/2/13

Jay McCarthy, … Jared Forsyth12

4/27/13

Remember, I expect your final turnins today

thought on "how much time do you spend" -- if you ask them to use git, and commit after

unread,

Remember, I expect your final turnins today

thought on "how much time do you spend" -- if you ask them to use git, and commit after

4/27/13

4/26/13

Re: Abridged summary of byu-cs-430-winter-2013@googlegroups.com - 3 Messages in 1 Topic

I definitely won't give anyone less than the earlier functions. On Fri, Apr 26, 2013 at 7:22 AM,

unread,

Re: Abridged summary of byu-cs-430-winter-2013@googlegroups.com - 3 Messages in 1 Topic

I definitely won't give anyone less than the earlier functions. On Fri, Apr 26, 2013 at 7:22 AM,

4/26/13

4/15/13

http://faculty.cs.byu.edu/~jay/video/2013-Winter-430-14M.webm -- Jay McCarthy <j...@cs.byu.edu>

unread,

http://faculty.cs.byu.edu/~jay/video/2013-Winter-430-14M.webm -- Jay McCarthy <j...@cs.byu.edu>

4/15/13

Jared Forsyth, … Jay McCarthy8

4/13/13

Final, Submission deadline

24th On Saturday, April 13, 2013, Alyssa Meservy wrote: Meaning the 17th or 24th? On Sat, Apr 13,

unread,

Final, Submission deadline

24th On Saturday, April 13, 2013, Alyssa Meservy wrote: Meaning the 17th or 24th? On Sat, Apr 13,

4/13/13

4/12/13

http://en.wikipedia.org/wiki/Zipper_(data_structure) -- Jay McCarthy <j...@cs.byu.edu> Assistant

unread,

http://en.wikipedia.org/wiki/Zipper_(data_structure) -- Jay McCarthy <j...@cs.byu.edu> Assistant

4/12/13

4/12/13

Amazing "learning" algorithm

http://www.youtube.com/watch?v=xOCurBYI_gY http://www.cs.cmu.edu/~tom7/mario/mario.pdf -- Jay

unread,

Amazing "learning" algorithm

http://www.youtube.com/watch?v=xOCurBYI_gY http://www.cs.cmu.edu/~tom7/mario/mario.pdf -- Jay

4/12/13

4/9/13

I'm bringing some chow to class to celebrate tomorrow being an awesome day - let me know if there

unread,

I'm bringing some chow to class to celebrate tomorrow being an awesome day - let me know if there

4/9/13

4/8/13

Here's a simple verified and extracted type checker in Coq. https://github.com/jeapostrophe/exp/

unread,

Here's a simple verified and extracted type checker in Coq. https://github.com/jeapostrophe/exp/

4/8/13

4/5/13

http://faculty.cs.byu.edu/~jay/video/2013-Winter-430-12F.webm -- Jay McCarthy <j...@cs.byu.edu>

unread,

http://faculty.cs.byu.edu/~jay/video/2013-Winter-430-12F.webm -- Jay McCarthy <j...@cs.byu.edu>

4/5/13

4/5/13

I looked up the solution

We were on the right track, it's just not simple because there's a lot of busy work that I

unread,

I looked up the solution

We were on the right track, it's just not simple because there's a lot of busy work that I

4/5/13

Jay McCarthy, Jared Forsyth2

4/2/13

Remaining points

awesome thanks! On Monday, April 1, 2013 10:07:52 AM UTC-6, Jay McCarthy wrote: This table shows the

unread,

Remaining points

awesome thanks! On Monday, April 1, 2013 10:07:52 AM UTC-6, Jay McCarthy wrote: This table shows the

4/2/13

Daniel Haskin, Jay McCarthy3

3/29/13

Wierd error in Equiv.v

That's really strange. I don't see the same problem on my side with coqc. I wonder if the IDE

unread,

Wierd error in Equiv.v

That's really strange. I don't see the same problem on my side with coqc. I wonder if the IDE

3/29/13

3/27/13

http://faculty.cs.byu.edu/~jay/video/2013-Winter-430-11W.webm -- Jay McCarthy <j...@cs.byu.edu>

unread,

http://faculty.cs.byu.edu/~jay/video/2013-Winter-430-11W.webm -- Jay McCarthy <j...@cs.byu.edu>

3/27/13

Andrew Kent, Jay McCarthy2

3/25/13

redo_determinism...?

I think it is a typo in the textbook generator script and the proof sketch wasn't meant to be

unread,

redo_determinism...?

I think it is a typo in the textbook generator script and the proof sketch wasn't meant to be

3/25/13

3/25/13

I just pushed a fix to the script

It failed to parse some parts of Hoare -- Jay McCarthy <j...@cs.byu.edu> Assistant Professor /

unread,

I just pushed a fix to the script

It failed to parse some parts of Hoare -- Jay McCarthy <j...@cs.byu.edu> Assistant Professor /

3/25/13

3/22/13

Finished proof from class

Definition fact_inv (x : nat) : Assertion := fun st => (st Y) * (real_fact (st Z)) = real_fact x.

unread,

Finished proof from class

Definition fact_inv (x : nat) : Assertion := fun st => (st Y) * (real_fact (st Z)) = real_fact x.

3/22/13

3/20/13

Video: http://faculty.cs.byu.edu/~jay/video/2013-Winter-430-10W.webm Score function: https://github.

unread,

Video: http://faculty.cs.byu.edu/~jay/video/2013-Winter-430-10W.webm Score function: https://github.

3/20/13

3/19/13

I updated sf-check because of a mis-labeled theorem in Hoare.v

-- Jay McCarthy <j...@cs.byu.edu> Assistant Professor / Brigham Young University http://faculty.

unread,

I updated sf-check because of a mis-labeled theorem in Hoare.v

-- Jay McCarthy <j...@cs.byu.edu> Assistant Professor / Brigham Young University http://faculty.

3/19/13

3/15/13

http://faculty.cs.byu.edu/~jay/video/2013-Winter-430-9F.webm -- Jay McCarthy <j...@cs.byu.edu>

unread,

http://faculty.cs.byu.edu/~jay/video/2013-Winter-430-9F.webm -- Jay McCarthy <j...@cs.byu.edu>

3/15/13

3/13/13

So sick. I won't be able to teach Wed, so sorry.

-- Jay McCarthy <j...@cs.byu.edu> Assistant Professor / Brigham Young University http://faculty.

unread,

So sick. I won't be able to teach Wed, so sorry.

-- Jay McCarthy <j...@cs.byu.edu> Assistant Professor / Brigham Young University http://faculty.

3/13/13

Jay McCarthy, … Andrew Kent5

3/12/13

Video for today

Thank you very much, sir! You are a gentleman and a scholar! > Date: Tue, 12 Mar 2013 12:38:52 -

unread,

Video for today

Thank you very much, sir! You are a gentleman and a scholar! > Date: Tue, 12 Mar 2013 12:38:52 -

3/12/13

3/8/13

Fast inverse square root

http://en.wikipedia.org/wiki/Fast_inverse_square_root -- Jay McCarthy <j...@cs.byu.edu>

unread,

Fast inverse square root

http://en.wikipedia.org/wiki/Fast_inverse_square_root -- Jay McCarthy <j...@cs.byu.edu>

3/8/13

3/8/13

http://faculty.cs.byu.edu/~jay/video/2013-Winter-430-8F.webm Also, a note: (* P \/ Q -> R *) (*

unread,

http://faculty.cs.byu.edu/~jay/video/2013-Winter-430-8F.webm Also, a note: (* P \/ Q -> R *) (*

3/8/13

3/6/13

The video was successful. Uncompressed: 4.7G Compressed:110M Compression time: 3552.30s user 6.33s

unread,

The video was successful. Uncompressed: 4.7G Compressed:110M Compression time: 3552.30s user 6.33s

3/6/13

Jared Forsyth, Jay McCarthy2

3/4/13

"exists x." Where x is what you want it to be On Monday, March 4, 2013, Jared Forsyth wrote

unread,

"exists x." Where x is what you want it to be On Monday, March 4, 2013, Jared Forsyth wrote

3/4/13

Jay McCarthy, Dan Burton3

3/4/13

Video for class today...

I just figured out the correct settings to use next time... so I will probably have a good video on

unread,

Video for class today...

I just figured out the correct settings to use next time... so I will probably have a good video on

3/4/13

3/1/13

Code from class

I added an example of doing coinduction in a proof. Jay Inductive ceval_small : com -> state ->

unread,

Code from class

I added an example of doing coinduction in a proof. Jay Inductive ceval_small : com -> state ->

3/1/13

2/27/13

Updated extra code

Inductive ceval_small : com -> state -> com -> state -> Prop := | ES_Ass : forall st a1 n

unread,

Updated extra code

Inductive ceval_small : com -> state -> com -> state -> Prop := | ES_Ass : forall st a1 n

2/27/13

2/25/13

Extra stuff from today

Inductive ceval_small : com -> state -> com -> state -> Prop := | ES_Ass : forall st a1 n

unread,

Extra stuff from today

Inductive ceval_small : com -> state -> com -> state -> Prop := | ES_Ass : forall st a1 n

2/25/13

Search

Clear search

Close search

Google apps

Main menu