Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Contribute to GitLab
Sign in
Toggle navigation
C
cpdt
Project
Project
Details
Activity
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Board
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
research
cpdt
Commits
044ab374
Commit
044ab374
authored
Apr 22, 2012
by
Adam Chlipala
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Citations for continuations and unification
parent
dd36e329
Changes
4
Show whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
43 additions
and
4 deletions
+43
-4
cpdt.bib
latex/cpdt.bib
+39
-0
Match.v
src/Match.v
+1
-1
Predicates.v
src/Predicates.v
+2
-2
StackMachine.v
src/StackMachine.v
+1
-1
No files found.
latex/cpdt.bib
View file @
044ab374
...
@@ -375,3 +375,42 @@ year = {2010},
...
@@ -375,3 +375,42 @@ year = {2010},
publisher = {Springer-Verlag},
publisher = {Springer-Verlag},
address = {London, UK, UK},
address = {London, UK, UK},
}
}
@article{continuations,
author = {Reynolds, John C.},
title = {The discoveries of continuations},
journal = {Lisp Symb. Comput.},
issue_date = {Nov. 1993},
volume = {6},
number = {3-4},
month = nov,
year = {1993},
issn = {0892-4635},
pages = {233--248},
numpages = {16},
url = {http://dx.doi.org/10.1007/BF01019459},
doi = {10.1007/BF01019459},
acmid = {198114},
publisher = {Kluwer Academic Publishers},
address = {Hingham, MA, USA},
keywords = {continuation, continuation-passing style, semantics},
}
@article{unification,
author = {Robinson, J. A.},
title = {A Machine-Oriented Logic Based on the Resolution Principle},
journal = {J. ACM},
issue_date = {Jan. 1965},
volume = {12},
number = {1},
month = jan,
year = {1965},
issn = {0004-5411},
pages = {23--41},
numpages = {19},
url = {http://doi.acm.org/10.1145/321250.321253},
doi = {10.1145/321250.321253},
acmid = {321253},
publisher = {ACM},
address = {New York, NY, USA},
}
src/Match.v
View file @
044ab374
...
@@ -471,7 +471,7 @@ Abort.
...
@@ -471,7 +471,7 @@ Abort.
Even
basic
[
idtac
]
is
an
embedded
imperative
program
,
so
we
may
not
automatically
mix
it
with
purely
functional
code
.
In
fact
,
a
semicolon
operator
alone
marks
a
span
of
Ltac
code
as
an
embedded
tactic
script
.
This
makes
some
amount
of
sense
,
since
pure
functional
languages
have
no
need
for
sequencing
:
since
they
lack
side
effects
,
there
is
no
reason
to
run
an
expression
and
then
just
throw
away
its
value
and
move
on
to
another
expression
.
Even
basic
[
idtac
]
is
an
embedded
imperative
program
,
so
we
may
not
automatically
mix
it
with
purely
functional
code
.
In
fact
,
a
semicolon
operator
alone
marks
a
span
of
Ltac
code
as
an
embedded
tactic
script
.
This
makes
some
amount
of
sense
,
since
pure
functional
languages
have
no
need
for
sequencing
:
since
they
lack
side
effects
,
there
is
no
reason
to
run
an
expression
and
then
just
throw
away
its
value
and
move
on
to
another
expression
.
The
solution
is
like
in
Haskell
:
we
must
%
``
%
#
"#monadify#"
#
%
''
%
our
pure
program
to
give
it
access
to
side
effects
.
The
trouble
is
that
the
embedded
tactic
language
has
no
[
return
]
construct
.
Proof
scripts
are
about
proving
theorems
,
not
calculating
results
.
We
can
apply
a
somewhat
awkward
workaround
that
requires
translating
our
program
into
%
\
index
{
continuation
-
passing
style
}
\
emph
{%
#
<
i
>
#
continuation
-
passing
style
#
</
i
>
#
%}%,
a
program
structuring
idea
popular
in
functional
programming
.
*
)
The
solution
is
like
in
Haskell
:
we
must
%
``
%
#
"#monadify#"
#
%
''
%
our
pure
program
to
give
it
access
to
side
effects
.
The
trouble
is
that
the
embedded
tactic
language
has
no
[
return
]
construct
.
Proof
scripts
are
about
proving
theorems
,
not
calculating
results
.
We
can
apply
a
somewhat
awkward
workaround
that
requires
translating
our
program
into
%
\
index
{
continuation
-
passing
style
}
\
emph
{%
#
<
i
>
#
continuation
-
passing
style
#
</
i
>
#
%}
~
\
cite
{
continuations
}
%,
a
program
structuring
idea
popular
in
functional
programming
.
*
)
(
*
begin
hide
*
)
(
*
begin
hide
*
)
Reset
length
.
Reset
length
.
...
...
src/Predicates.v
View file @
044ab374
(
*
Copyright
(
c
)
2008
-
201
1
,
Adam
Chlipala
(
*
Copyright
(
c
)
2008
-
201
2
,
Adam
Chlipala
*
*
*
This
work
is
licensed
under
a
*
This
work
is
licensed
under
a
*
Creative
Commons
Attribution
-
Noncommercial
-
No
Derivative
Works
3.0
*
Creative
Commons
Attribution
-
Noncommercial
-
No
Derivative
Works
3.0
...
@@ -892,7 +892,7 @@ Theorem even_contra : forall n, even (S (n + n)) -> False.
...
@@ -892,7 +892,7 @@ Theorem even_contra : forall n, even (S (n + n)) -> False.
intros
;
eapply
even_contra
'
;
eauto
.
intros
;
eapply
even_contra
'
;
eauto
.
Qed
.
Qed
.
(
**
We
use
a
variant
%
\
index
{
tactics
!
apply
}%
[
eapply
]
of
[
apply
]
which
has
the
same
relationship
to
[
apply
]
as
[
eauto
]
has
to
[
auto
]
.
An
invocation
of
[
apply
]
only
succeeds
if
all
arguments
to
the
rule
being
used
can
be
determined
from
the
form
of
the
goal
,
whereas
[
eapply
]
will
introduce
unification
variables
for
undetermined
arguments
.
In
this
case
,
[
eauto
]
is
able
to
determine
the
right
values
for
those
unification
variables
.
(
**
We
use
a
variant
%
\
index
{
tactics
!
apply
}%
[
eapply
]
of
[
apply
]
which
has
the
same
relationship
to
[
apply
]
as
[
eauto
]
has
to
[
auto
]
.
An
invocation
of
[
apply
]
only
succeeds
if
all
arguments
to
the
rule
being
used
can
be
determined
from
the
form
of
the
goal
,
whereas
[
eapply
]
will
introduce
unification
variables
for
undetermined
arguments
.
In
this
case
,
[
eauto
]
is
able
to
determine
the
right
values
for
those
unification
variables
,
using
(
unsurprisingly
)
a
variant
of
the
classic
algorithm
for
%
\
emph
{%
#
<
i
>
#
unification
#
</
i
>
#
%}~
\
cite
{
unification
}%
.
By
considering
an
alternate
attempt
at
proving
the
lemma
,
we
can
see
another
common
pitfall
of
inductive
proofs
in
Coq
.
Imagine
that
we
had
tried
to
prove
[
even_contra
'
]
with
all
of
the
[
forall
]
quantifiers
moved
to
the
front
of
the
lemma
statement
.
*
)
By
considering
an
alternate
attempt
at
proving
the
lemma
,
we
can
see
another
common
pitfall
of
inductive
proofs
in
Coq
.
Imagine
that
we
had
tried
to
prove
[
even_contra
'
]
with
all
of
the
[
forall
]
quantifiers
moved
to
the
front
of
the
lemma
statement
.
*
)
...
...
src/StackMachine.v
View file @
044ab374
...
@@ -814,7 +814,7 @@ Abort.
...
@@ -814,7 +814,7 @@ Abort.
Lemma
tcompile_correct
'
:
forall
t
(
e
:
texp
t
)
ts
(
s
:
vstack
ts
)
,
Lemma
tcompile_correct
'
:
forall
t
(
e
:
texp
t
)
ts
(
s
:
vstack
ts
)
,
tprogDenote
(
tcompile
e
ts
)
s
=
(
texpDenote
e
,
s
)
.
tprogDenote
(
tcompile
e
ts
)
s
=
(
texpDenote
e
,
s
)
.
(
**
While
lemma
[
compile_correct
'
]
quantified
over
a
program
that
is
the
%
``
%
#
"#continuation#"
#
%
''
%
for
the
expression
we
are
considering
,
here
we
avoid
drawing
in
any
extra
syntactic
elements
.
In
addition
to
the
source
expression
and
its
type
,
we
also
quantify
over
an
initial
stack
type
and
a
stack
compatible
with
it
.
Running
the
compilation
of
the
program
starting
from
that
stack
,
we
should
arrive
at
a
stack
that
differs
only
in
having
the
program
'
s
denotation
pushed
onto
it
.
(
**
While
lemma
[
compile_correct
'
]
quantified
over
a
program
that
is
the
%
``
%
#
"#continuation#"
#
%
''
~
\
cite
{
continuations
}
%
for
the
expression
we
are
considering
,
here
we
avoid
drawing
in
any
extra
syntactic
elements
.
In
addition
to
the
source
expression
and
its
type
,
we
also
quantify
over
an
initial
stack
type
and
a
stack
compatible
with
it
.
Running
the
compilation
of
the
program
starting
from
that
stack
,
we
should
arrive
at
a
stack
that
differs
only
in
having
the
program
'
s
denotation
pushed
onto
it
.
Let
us
try
to
prove
this
theorem
in
the
same
way
that
we
settled
on
in
the
last
section
.
*
)
Let
us
try
to
prove
this
theorem
in
the
same
way
that
we
settled
on
in
the
last
section
.
*
)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment