[TYPES] Fwd: When types appeared in programming languages

PATRICK BROWNE patrick.browne at dit.ie
Fri Oct 16 07:48:16 EDT 2015


Simone,
I enjoyed your review of types. Have you looked at Joseph Goguen's paper
Type as Theories[1].
He presents three descriptions of types: 1)as sets, 2)as algebras, 3)as
theories.
I believe that algebraic languages like CafeOBJ and Maude support all three
approach to types.
Types as sets: Using *sorts*, which can be arrange in a lattice of sorts.
Types as algebras: Tight modules with carrier set, and concrete operations
using initial semantics
Types as theories: Loose modules representing theories with axioms stating
properties e.g. partial order, monoid.
                   Types are logical theories, presented by axioms, whose
properties can be explored by logical deduction.
Regards,
Pat
[1]
http://www.google.ie/url?sa=t&rct=j&q=&esrc=s&source=web&cd=4&cad=rja&uact=8&ved=0CDQQFjADahUKEwib3eGM1MbIAhXC6xQKHcsLA4A&url=http%3A%2F%2Fciteseerx.ist.psu.edu%2Fviewdoc%2Fdownload%3Fdoi%3D10.1.1.16.2241%26rep%3Drep1%26type%3Dps&usg=AFQjCNGjxJGhAumTd7mV0iNovz3eKUco3g&bvm=bv.105039540,d.d24

On 14 October 2015 at 10:26, Simone Martini <simone.martini at unibo.it> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> Last year, there has been a thread on this mailing list on the role (and
> concept) of types in programming languages, started by this msg of Vladimir
> Voevodsky:
>         http://lists.seas.upenn.edu/pipermail/types-list/2014/001745.html
>
> Stimulated from that thread (which showed that there was little consensus
> on when types appeared, and with which meaning), I wrote a little essay,
> suggesting that the emergence of the concept of type in computer science is
> relatively independent from the logical tradition, until the Curry-Howard
> isomorphism will make an explicit bridge between them.
>
> I presented the paper last week at History and Philosophy of Computing
> 2015, in Pisa.
>
>         http://arxiv.org/abs/1510.03726
>
> Comments, remarks, and especially critiques would be much welcomed from
> the members of this list.
>
> Best,
> -s.
> ---------------------------------------------------
> Simone Martini
> Universita' di Bologna
> Dip. di Informatica - Scienza e Ingegneria
> Italy
>
> www.cs.unibo.it/~martini
>

-- 


This email originated from DIT. If you received this email in error, please 
delete it from your system. Please note that if you are not the named 
addressee, disclosing, copying, distributing or taking any action based on 
the contents of this email or attachments is prohibited. www.dit.ie

Is ó ITBÁC a tháinig an ríomhphost seo. Má fuair tú an ríomhphost seo trí 
earráid, scrios de do chóras é le do thoil. Tabhair ar aird, mura tú an 
seolaí ainmnithe, go bhfuil dianchosc ar aon nochtadh, aon chóipeáil, aon 
dáileadh nó ar aon ghníomh a dhéanfar bunaithe ar an ábhar atá sa 
ríomhphost nó sna hiatáin seo. www.dit.ie

Tá ITBÁC ag aistriú go Gráinseach Ghormáin – DIT is on the move to 
Grangegorman <http://www.dit.ie/grangegorman>


More information about the Types-list mailing list