Re: [TYPES] TaPL Course?

[Alejandro Díaz-Caro]

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

Hi Robert,

I give a course at a degree in programming at Quilmes University, using
typed lambda calculus.

The webpage and notes (in Spanish) is here:
https://urldefense.com/v3/__http://clp.web.unq.edu.ar/apuntes-y-practicas/__;!!IBzWLUs!XAPllmUn3YsWKjEpx23e80cVtUf6jfRHZp_x1BoCh6HDYQI2H6l5-PdbaijzRqcyEpv0KoEUIJVYhC1Mg4-z_tXDECi_9hmGGn4L$
 

However, the notes are mostly based on the following very nice book:

G. Dowek & J.-J. Levy, Introduction to the theory of programming languages,
Springer, 2011

Fell free to use the exercises or any material if it suits the topics you
plan to cover.

Best,
Alejandro

--
Sent from my mobile (i.e. sorry for the bad autocorrections)

El sáb, 17 dic. 2022 05:20, Robert Rand  escribió:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Hi,
>
> I was wondering who is teaching a programming languages course using Types
> and Programming Languages? I'm planning on teaching such a course at
> UChicago this Spring (March - June) and I'm looking for inspiration and
> suggestions. If you're on the quarter system and/or have material you'd
> like to share, that's especially welcome!
>
> Thanks!
> Robert
>

Re: [TYPES] R: ETAPS bars Russian researchers from attending

[Alejandro Díaz-Caro]

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

Dear Marino, dear all,

El mié, 9 mar. 2022 05:05, Marino Miculan 
escribió:

>
> Of course, I am sure that there are many colleagues there against the
> invasion. But then, we have to distinguish between the responsibility of
> the single, and that of the institution.  For instance, I would have no
> problems if a researcher from a Russian university  registers and presents
> their results at ETAPS (or any other conference) without​ any affiliation.
> That would be already a strong signal, as in "I'm here on my own, and I
> dissociate from my rector's opinions".
>

That would be even worst than the decision of banning a country by their
war politics. What you are proposing there is to ask the researchers about
their political personal opinion in order to be admitted to a conference. I
find this completely wrong.

Shall we also inquire Cubans if they support Fidel Castro or Americans if
they support the blockade? Shall we ask Israel or Palestinians what side of
the conflict they support, and let them register according to the personal
stand of the organisers at the venue?

I think that mixing politics with the scientific community at this global
level is very dangerous and ultimately wrong.

I hope this line of actions do not prosper, or we will damage the
scientific community for many years.

Best,
Alejandro

>

Re: [TYPES] online conferences should be free

[Alejandro Díaz-Caro]

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

I may add that it makes totally sense to me that a service such as Clowdr
(and other similar platforms) charge for their usage. The price do not only
covers the usage, but also there is somebody to assist you (giving
tutorials, answering questions, etc). In any case the prices are quite fair
and, as I mentioned before, there are still options to make the conference
either free, or mostly free. The alternative would be to use some ad-hoc
solution, which probably will not be perfectly adapted for a conference.
And since conferences will be virtual yet for some time (at least), we
should use the best available tools.

So, my point of view is that conferences should be free, as much as
possible, and should not renounce to use the best available tools.

-- Alejandro


El dom., 6 jun. 2021 20:33, Benjamin Pierce 
escribió:

> On Sun, Jun 6, 2021 at 1:15 AM Stefan Monnier 
> wrote:
>
>> [ The Types Forum,
>> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>> I think it would make sense for the ACM to host some of those services
>> (and participate in their development).  IIUC this is partly what
>> happen(s|ed) with clowdr.
>>
>
> I can say a few words about what happened with Clowdr... :-)
>
> For those that don't know, Clowdr  is an open-source
> virtual conference platform that's been under development for the past year.
>
> The first version of Clowdr in summer 2020 was supported by a small NSF
> grant. Since the autumn, further development has been led by Clowdr CIC, a
> UK Community Interest Company that was set up to maintain, develop, and
> help conferences use Clowdr. The company has grown organically, funded by
> service contracts with individual conferences under which Clowdr hosts the
> platform and, in some cases, assists with conference organization and
> logistics. Several of these have been ACM conferences, but the company has
> never received funding or sponsorship directly from ACM.
>
> Best,
>
> - Benjamin
>
> P.S. For full disclosure, I am one of the original Clowdr developers and
> one of the founding directors of Clowdr CIC. To avoid conflicts of
> interest, I resigned all my official positions within ACM and SIGPLAN when
> the company was formed.
>
>
>
>

Re: [TYPES] online conferences should be free (was: global debriefing over our virtual experience of conferences)

[Alejandro Díaz-Caro]

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

Dear all,

The real costs of online conferences are much less than for physical
ones, that is clear. However, it is not free of cost. The costs may
be:
* Publication costs (for example, LIPIcs charges 60 euros per paper)
* Easychair licence
* Award prize for best paper (if the conference have this kind of award)
* Conference platform costs (Clowdr, Slack, Zoom, GatherTown, etc, all
have an associated cost).

>From these four, the first three are somehow fixed with the number of
accepted papers (which is usually similar from one year to the next).
However the last one is the more difficult to predict, since platforms
such as Clowdr, GatherTown, or Easychar's VCS charge per person
(Easychair's VCS even charges per person per day). So, even if you get
funding from the organising institution or sponsors, making it free of
charge could imply a really big amount of registrations, and you may
pay for those even if they do not show up at the conference.

The solution that we chose at FSCD this year is to make it free of
charge, unless we receive way too many requests (with "way too many"
left undefined yet), surpassing the grants we have got for the
conference. In such a case, we will ask for  a very modest amount
(less than 10 dollars), making it clear that those who cannot pay, can
participate enterally free of charge. So, we are hoping to have a
fully free of charge conference (and quite probably we will), but we
have no idea how many people will register and how much the bill at
the chosen platform may grow.

Of course there are also free platforms, but they are less reliable
and you do not have anyone to ask if things do not work as expected.

Coming from Argentina, I agree that conferences (specially virtual)
should be free of charge or as cheap as they can, as much as they can.
This allows students to participate. I also agree that the slogan "you
will pay more attention to what you have paid" should not condition
our conferences model. Paying attention to talks is a responsibility
(or a choice) of the attendee (and of the speaker to make the talk
interesting, maybe). Putting money in the middle to encourage it is
not the best practice, in my opinion, especially if that could result
in people left behind.

Best,
Alejandro


On Fri, 4 Jun 2021 at 15:28, Mehmet Oguz Derin
 wrote:
>
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Outsider opinion: one good heuristic for pricing anything virtual and
> making it accessible for underprivileged individuals is localized video
> game & digital subscription prices. Companies expanding these have gone
> through many stages regarding price localization (symbolic or not)
> globally. - Oguz (Mehmet Oguz Derin)
>
> On Fri, Jun 4, 2021 at 4:18 PM Gabriel Scherer 
> wrote:
>
> > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> > ]
> >
> > Dear list,
> >
> > Last year I played the unfortunate role of complaining about the $100 price
> > tag on ICFP'20 registration. There were some great improvements in further
> > events, for example POPL'21 had "discounted rate: $10" as an unconditional
> > registration option, and PLDI'21 offers the same option. (I still wish that
> > there events were free, as is common with other scientific conferences like
> > FSCD'20, IJCAR'20, LICS'20 etc., but $10 is still much closer to a symbolic
> > sum than $100 for a strict subset of the world.).
> >
> > Unfortunately, it is my understanding that ICFP'21 is planning to reuse the
> > same fee structure. The details are not clear yet and possibly subject to
> > change, as registration hasn't opened; but this seems to be the current
> > plan. I wish it was possible to have a (public) discussion about this
> > choice in advance, and not just a month or two before the conference during
> > summer holidays.
> >
> > SIGPLAN has decided not to publish budget information for ICFP'20, but my
> > understanding is that the $100 registration scheme generated a strong
> > profit for the conference, to the point that, if the costs are comparable
> > to last year, last year profit would suffice to fund ICFP'21 entirely. Why
> > would we have a $100 registration fee again?
> >
> > ICFP is a flagship conference at the intersection of theoretical works and
> > practical functional programming, and it could attract a vibrant crowd of
> > people outside academia (in particular: not students), who may not have an
> > easy path to reimbursement -- this is especially important for the
> > workshops.
> >
> > (Disclaimer: I'm criticising past registration fees and prospective
> > registration fees, but not of course the people doing the hard work of
> > organizing the conference! They have all my gratitude.)
> >
> > On Sun, Aug 23, 2020 at 4:05 PM Gabriel Scherer  > >
> > wrote:
> >
> > > Dear types-list,
> > >
> > > Going on a tangent from Flavien's earlier post: I really think 

Re: [TYPES] System F and System T names

[Alejandro Díaz-Caro]

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

Dear Neel,

Thank you for the info. That is exactly what I was looking for.

Kind regards,
Alejandro

On Fri, 6 Apr 2018 at 14:03 Neel Krishnaswami <
neelakantan.krishnasw...@gmail.com> wrote:

> Hello,
>
> 1. In "The system F of variable types, fifteen years later", Girard
> remarks  that there was no particular reason for the name F:
>
> However, in [3] it was shown that the obvious rules of conversion for
> this system, called F by chance, were converging.
>
> There may be another explanation in his thesis, but I haven't read it
> since unfortunately I am not fluent in French.
>
> 2. However, since I am semiliterate in German, I did take a look at
> Gödel's paper "Über eine noch nicht benüzte Erweiterung des finiten
> Standpunktes", where System T (and the Dialectia interpretation for it)
> was introduced. He names this system in a parenthetical aside:
>
>Das heisst die Axiome dieses Systems (es werde T genannt) sind formal
>fast dieselben wie die der primitiv rekursiven Zahlentheorie [...][1]
>
> However, the previous page and a half were spent talking about the type
> structure of system T, so it is reasonable to guess that T stands for
> "types". But, no explicit reason is given in print.
>
> Best,
> Neel
>
>
> [1] "This means the axioms of this system (dubbed T) are nearly
> the same as those of primitive recursive number theory [...]"
>
> On 06/04/18 12:07, Alejandro Díaz-Caro wrote:
> > [ The Types Forum,
> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> >
> > Dear Type-theorists,
> >
> > Does anyone know where do the names System "F" and System "T" comes
> from? I
> > am not asking who introduced those names (Girard System F, and Gödel
> System
> > T), but what the "F" and the "T" means.
> >
> > Kind regards,
> > Alejandro
> >
>
-- 

http://diaz-caro.web.unq.edu.ar

[TYPES] System F and System T names

[Alejandro Díaz-Caro]

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

Dear Type-theorists,

Does anyone know where do the names System "F" and System "T" comes from? I
am not asking who introduced those names (Girard System F, and Gödel System
T), but what the "F" and the "T" means.

Kind regards,
Alejandro
-- 

http://diaz-caro.web.unq.edu.ar