headers
Paweł Urzyczyn | 1 May 2013 14:02
Picon
Picon

[TYPES] Future of TLCA

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

This message is addressed to everyone interested in the future
of the conference TLCA (Typed Lambda Calculi and Applications).
The bi-annual conference started in 1993 and will have its 11th
edition this June in Eindhoven as part of RDP. After 20 years
it seems reasonable to ask some questions about the future.
In particular there is an emerging discussion on whether TLCA
should merge with RTA or perhaps develop into a new conference
of a broader scope. In order to gain opinions from as large part
of TLCA community as possible, we have created a Google Group:

     https://groups.google.com/forum/#!forum/tlca-list

We invite everybody who feels part of TLCA community to contribute
to the discussion with their opinions and suggestions.

Samson Abramsky, Pierre-Louis Curien,
Mariangiola Dezani-Ciancaglini,
Masahito Hasegawa, Luke Ong,
Simona Ronchi Della Rocca,
Paweł Urzyczyn
Permalink | Reply | 1 comment |
headers
Uday S Reddy | 29 Apr 2013 21:39
Picon
Picon
Favicon

[TYPES] John Reynolds

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear friends and colleagues,

I am sorry to bring the sad news that John Reynolds, whose work and insights
I have mentioned and recounted in my recent exchanges, has passed away on
Sunday in Pittsburgh.

John has not only done seminal work on a wide range of programming language
topics, but he was also a guiding spirit and a great friend to many of us.
We will dearly miss him.

At this juncture, we might take a moment to reflect on his life time of
accomplishment:

  http://www.cs.cmu.edu/~jcr/

Uday

--

-- 
Prof. Uday Reddy                Tel: +44 121 414 2740             
Professor of Computer Science   Fax: +44 121 414 4281
School of Computer Science      Email: U.S.Reddy@...
University of Birmingham        
Edgbaston                       
Birmingham B15 2TT              Web: http://www.cs.bham.ac.uk/~udr
Permalink | Reply | 1 comment |
headers
Mark Janssen | 23 Apr 2013 19:02
Picon
Gravatar

Re: [TYPES] Declarative vs imperative

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

>> But there are no details left out.  Neither the computer nor compiler
>> "fills in the gaps".  What computing devices are you talking about?
>> At every step, at the various levels of abstraction, from the
>> high-level source code, to the the binary executable, there is a
>> complete and detailed "transformation" logic.   It will compile down
>> to the same machine code *every* time, if it's working properly.
>
> Are you claiming, then, that all those fancy optimization flags I can pass to my C compiler don't actually
do anything? Or that (say) -fomit-frame-pointer is unfaithful to the "complete and detailed
transformation logic"? Better file a bug report.

I well aware of compiler flags and was not implying at all that they
don't do anything.  What I was saying is that the compilers output is
deterministic.  If you use the same flags and the same source, you
will get the same output -- unless you're suggesting some *magic
happens here* event.

MarkJ
Tacoma, Washington
Permalink | Reply | 6 comments |
headers
Adam Smith | 22 Apr 2013 23:27
Gravatar

Re: [TYPES] [tag] Re: Declarative vs imperative

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

(resending after actually signing up for types-list)

Vladimir's way distinguishing declarative vs imperative programs is indeed
clear-cut, but let me offer an explanation why it's not going to convince
every programmer or language designer. The key idea is that languages of
one type are usually rich enough enough to support an embedded language of
the other type (or possibly many layers like this), and the experience of
the programmer/designer may so strongly focus on the embedded languages
that the properties of the outer language become largely inconsequential.

Concretely, if you come across a large collection of declarative statements
that are semantically about imperative commands, you start to simply read
through the declarative aspects and see the imperative program as the real
one. Here are a bunch of declarative statements (that are simply true):

~ The first step of the algorithm is to set a variable called "maxlen" to
"0".
~ The second step of is to enact a for-loop over the variable "j" from "0"
to "2".
~ The body of this loop is the action of setting "maxlen" to the maximum of
the value of "maxlen" and the length of input value "j".

The following example is from an on-going project involving using answer
set programming to reason about the different possible execution paths
through imperative code. At the surface level, it's just one giant
declarative AnsProlog fact that states that "add(....) is a procedure". For
all other purposes (including capturing an idea in code and debugging its
representation on the basis of it's example executions), it's a pile of
(Continue reading)

Permalink | Reply | 0 comments |
headers
Mark Janssen | 20 Apr 2013 10:36
Picon
Gravatar

Re: [TYPES] The type/object distinction and possible synthesis of OOP and imperative programming languages

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

> I suggest you read more on sentential logic (which can be called "Zero-Order
> Logic", and which I think is what you mean by 'Boolean/Binary/Digital
> Logic')

While interesting (and thank you for the terms), I think I by Boolean
Logic, something different is meant.   In fact, perhaps we have hit
upon the exact point where the confusion lies.

The logic I'm talking about does not come out of philosophy like the
predicate calculii -- and it is not sentential *at all*.  I'm going to
refer to that with the more Greek spelling of "logik".

Boolean logic, is distinguished with, I'll claim, an entirely
different lexicon.  Now, this word set can be readily mapped to that
used in predicate calculus, but this ease is also the cause of the
confusion -- they are two different realms.

The primary difference in language to note is this one (put in
analogical form with predicate logic first):  true:false::1:0.  That
seems simple, but from there two completely different maths have been
made which are orthogonal to each other.

With the former, one never adds truth values together, for example,
but with the latter, that is about all you do.  Further, one never
negates the "true" to get "false" in sentential logic, but with
boolean logic, it is done routinely.  Boolean logic is often done in a
parallel fashion, hence one hears of 32-bit adders, but you would
never hear or conceive of such in predicate calculus.   The machines
(Continue reading)

Permalink | Reply | 0 comments |
headers
Mark Janssen | 15 Apr 2013 05:48
Picon
Gravatar

[TYPES] The type/object distinction and possible synthesis of OOP and imperative programming languages

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello,

I'm new to the list and hoping this might be the right place to
introduce something that has provoked a bit of an argument in my
programming community.

I'm from the Python programming community.  Python is an "interpreted"
language.  Since 2001, Python's has migrated towards a "pure" Object
model (ref: http://www.python.org/download/releases/2.2/descrintro/).
Prior to then, it had both types and classes and these types were
anchored to the underlying C code and the machine/hardware
architecture itself.  After the 2001 "type/class unification" , it
went towards Alan Kay's ideal of "everything is an object".  From
then, every user-defined class inherited from the abstract Object,
rooted in nothing but a pure abstract ideal.  The parser, lexer, and
such spin these abstrations into something that can be run on the
actual hardware.

As a contrast, this is very distinct from C++, where everything is
concretely rooted in the language's type model which in *itself* is
rooted (from it's long history) in the CPU architecture.   The STL,
for example, has many Container types, but each of them requires using
a single concrete type for homogenous containers or uses machine
pointers to hold arbitrary items in heterogeneous containers (caveat:
I haven't programmed in C++ for a long time, so it's possible this
might not be correct anymore).

My question is:  Is there something in the Computer Science literature
(Continue reading)

Permalink | Reply | 0 comments |
headers
Christian Skalka | 28 Jan 2013 23:38
Picon

[TYPES] Decidability of type reconstruction in predicative System-F?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I am wondering if there are formal results related to the (un?)decidability
of type reconstruction in predicative System-F. As I understand it, Joe
Wells' well-known undecidability result only applies to impredicative
System-F.

Pointers/citations appreciated.

Thanks,

-chris

--

-- 
Christian Skalka
Associate Professor
Department of Computer Science
University of Vermont
http://www.cs.uvm.edu/~skalka
Permalink | Reply | 2 comments |
headers
Andreas Abel | 11 Dec 2012 01:34
Picon
Favicon

[TYPES] Strong normalization of overlapping rewrite rules

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

The typical normalization proof for a typed lambda calculus with rewrite 
rules requires the rules to be left-linear and non-overlapping.  What is 
known about left-linear but /overlapping/ rewriting?  [References 
appreciated.]

Best,
Andreas

--

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel@...
http://www2.tcs.ifi.lmu.de/~abel/
Permalink | Reply | 1 comment |
headers
Derek Dreyer | 5 Dec 2012 14:42
Favicon

[TYPES] a counterexample to Plotkin and Abadi's characterization of equivalence at existential type?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I have what appears to be a counterexample to the characterization of
equivalence at existential type in Plotkin and Abadi's logic for
parametric polymorphism, and I'm wondering what's going on.  Here is a
link to their TLCA'93 paper from Gordon's web page:

http://homepages.inf.ed.ac.uk/gdp/publications/Par_Poly.pdf

In short, Theorem 7 in their paper says that two terms of existential
type are equal *if and only if* there exists a "simulation relation"
between their internal representations of the abstract type such that
the operations are logically related at the appropriate type
(interpreting the abstract type using the chosen simulation relation).
 The "if" direction is fine: that's just the well-known principle of
"representation independence".  It's the "only if" direction that I'm
confused about.

In particular, it seems to me that, using the "only if" direction of
Theorem 7, I can derive a contradiction in the logic, so I'm trying to
figure out where/if I screwed up.

The issue is the following: There is an example given in Pitts'
chapter in Pierce's ATTAPL book, namely Sumii's variation on Example
7.7.4 discussed in Remark 7.7.7.  (I will reproduce it below.)  The
entire point of the example, which in Sumii's variation applies to
pure System F, is that it shows a case where two existential packages
are contextually equivalent despite the fact that there is no
simulation relation between their type representations that would make
a simulation argument (i.e. representation independence proof) go
(Continue reading)

Permalink | Reply | 8 comments |
headers
George Cherevichenko | 4 Nov 2012 21:43
Picon

[TYPES] Please give me a link. Is alpha-conversion easy or not?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi
Where can I find a precise description how to interpret typed lambda
calculi with named variables in cartesian closed categories? Or how to
interpret lambda calculi with named variables in lambda calculi with De
Brujn indices? I know how to do that, but I need a link. I need proofs of
the following facts:
1) Alpha-equal terms correspond to the same term with De Brujn indices (or
the same arrow in CCC).
2) Substitutions with named variables correspond to substitutions with De
Brujn indices.
I read Altenkirch "Alpha-conversion is easy", should I only refer to this
article?
Please, no nominal logic.
George
Permalink | Reply | 2 comments |
headers
Ahn, Ki Yung | 17 Oct 2012 01:38
Picon

[TYPES] Free theorems for maps of higher rank and polarized systems?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I have some questions on free theorems for maps, which most people may 
believe, but having difficulty to cite where actual proof is written 
down, or an instance of a more general theorem, or whether it has ever 
been actually proved. I'd greatly appreciate pointers to related papers.

Question 1. Proper citation for free theorems for fmap
   (fmap is Haskell-ish term for generic maps) for rank 1
   (* -> *) and rank 2 (such as (* -> *) -> (* -> *))?

Wadler's "Theorems for free!" papers discusses map for lists.

But everyone seem to believe it holds for arbitrary structure of rank 1, 
that is, F : * -> *. We can formalize this idea in Fw as follows:

If there exists
   fmap : forall (f:*->*)(a:*)(b:*). (a -> b) -> f a -> f b
then (1) any such fmap satisfy the expected property of fmap, i.e.,
   fmap id = id
   fmap f . fmap f = fmap g
and  (2) also such fmap is unique.

Similar statement could be made for rank 2 version of this.
These generic maps of also called as monotonicity witness.

Papers on monotonicity that I've seen doesn't exactly proves (1) but 
since they use monotonicity witness to encode iterations or folds, I 
think it may be considered as indirect proof of the properties in (1). 
But it would be nice to know if you have seen proofs of statements in
(Continue reading)

Permalink | Reply | 0 comments |

Gmane