[icfp] nix the old abstract, need a new one
This commit is contained in:
parent
ad3b5a1305
commit
acaaa91349
|
@ -7,21 +7,22 @@
|
||||||
""]
|
""]
|
||||||
|
|
||||||
@title{Functional Pearl: Do you see what I see?}
|
@title{Functional Pearl: Do you see what I see?}
|
||||||
@subtitle{Improving a simple type system with dependent macros}
|
@; @subtitle{Improving a simple type system with dependent macros}
|
||||||
@; should say "value-dependent"?
|
@; should say "value-dependent"?
|
||||||
@; TODO subtitle doesn't appear in the right place
|
@; TODO subtitle doesn't appear in the right place
|
||||||
|
|
||||||
@abstract{
|
@abstract{
|
||||||
A simple type system with macros is nearly as good as a dependent type
|
TBA @; Be Positive, not negative
|
||||||
system, at least for some common programming tasks.
|
@;A simple type system with macros is nearly as good as a dependent type
|
||||||
By analyzing program syntax and propogating constants
|
@; system, at least for some common programming tasks.
|
||||||
before type-checking, we can express many of the practical
|
@;By analyzing program syntax and propogating constants
|
||||||
motivations for dependent types without any programmer annotations
|
@; before type-checking, we can express many of the practical
|
||||||
or extensions to the underlying type system.
|
@; motivations for dependent types without any programmer annotations
|
||||||
|
@; or extensions to the underlying type system.
|
||||||
|
|
||||||
Our syntax-dependent subtypes are not proving theorems,
|
@;Our syntax-dependent subtypes are not proving theorems,
|
||||||
but they detect certain run-time errors at compile-time and
|
@; but they detect certain run-time errors at compile-time and
|
||||||
cooperate with type inference.
|
@; cooperate with type inference.
|
||||||
}
|
}
|
||||||
|
|
||||||
@;@category["D.3.3" "Programming Languages" "Language Constructs and Features"]
|
@;@category["D.3.3" "Programming Languages" "Language Constructs and Features"]
|
||||||
|
|
Loading…
Reference in New Issue
Block a user