Subject: Foundational Methods in Computer Science Workshop
(FMCS'01) - msg#00008

Previous Message by Date:

Re: Barendregt was right after all ... almost

My student Jonathan Ford formalized CR using a single sort of named variables in PVS. His proof and the paper describing it is avaliable from http://mcs.une.edu.au/~pvs -- Dr Ian A. Mason. Convener and Postgraduate Coordinator Computer Science Division School of Mathematical & Computer Sciences University of New England Armidale 2351 N.S.W Australia phone: +61 (0)2 6773 2327 fax: +61 (0)2 6773 3312 iam-1KIrNqah8RGBkGSv8/8oeYdd74u8MsAO@xxxxxxxxxxxxxxxx http://mcs.une.edu.au/~iam/

Next Message by Date:

Re: positions at the Technical University of Denmark

[Type systems play a key role in reasoning about software and in enforcing adequate software development practices and more specifically in guaranteeing and enforcing security policies; for these reasons the following positions are relevant for applicants with a strong background in the use of type systems. / F. Nielson] The Technical University of Denmark is happy to announce a number of associate professorships (tenured) and assistant professorships (untenured) http://www.imm.dtu.dk/cst/jobs.htm covering data security, algorithmics, distributed systems, software engineering, embedded systems etc. The Technical University of Denmark was created in 1829 by the discoverer of electromagnetism, H.C.Oersted, and became the first private Danish University in 2001, thanks to a donation by the Danish Government, in order to increase its impact on research and teaching in engineering and science. The Department of Informatics & Mathematical Modelling has been given the mission to strengthen Computer Science and Technology and will be announcing a substantial number of positions within selected areas in the coming years. -- ---------------------------------------------------------------------- Professor dr.scient. Flemming Nielson direct: (+45) 4525 3735 Informatics & Mathematical Modelling mailto:nielson-hAEytp/1A71/SzgSGea1oA@xxxxxxxxxxxxxxxx The Technical University of Denmark http://www.imm.dtu.dk/~nielson ----------------------------------------------------------------------

Previous Message by Thread:

Barendregt was right after all ... almost

Dear Colleague, We are happy to announce the following two articles which might be of interest to the readers of the types and rewriting lists (and rush to apologise for multiple copies). Both are by Rene Vestergaard and James Brotherston and are available from http://iml.univ-mrs.fr/~vester/Writings/index.html. The articles are made available along with the associated Isabelle/HOL proof developments. In one sense, the articles provide a formal justification for the use of the informal notion referred to as the Barendregt Variable Convention. * A Formalised First-Order Confluence Proof for the lambda-Calculus Using One-Sorted Variable Names (Barendregt was right after all ... almost) --- to appear at RTA'01 * The Mechanisation of Barendregt-Style Equational Proofs (The Residual Perspective) --- preliminary version We know of no other formal proof developments of equational properties that are conducted directly on first-order abstract syntax with one-sorted variable names (but are naturally interested in any pointers). On behalf of the authors, /R

Next Message by Thread:

Re: positions at the Technical University of Denmark

[Type systems play a key role in reasoning about software and in enforcing adequate software development practices and more specifically in guaranteeing and enforcing security policies; for these reasons the following positions are relevant for applicants with a strong background in the use of type systems. / F. Nielson] The Technical University of Denmark is happy to announce a number of associate professorships (tenured) and assistant professorships (untenured) http://www.imm.dtu.dk/cst/jobs.htm covering data security, algorithmics, distributed systems, software engineering, embedded systems etc. The Technical University of Denmark was created in 1829 by the discoverer of electromagnetism, H.C.Oersted, and became the first private Danish University in 2001, thanks to a donation by the Danish Government, in order to increase its impact on research and teaching in engineering and science. The Department of Informatics & Mathematical Modelling has been given the mission to strengthen Computer Science and Technology and will be announcing a substantial number of positions within selected areas in the coming years. -- ---------------------------------------------------------------------- Professor dr.scient. Flemming Nielson direct: (+45) 4525 3735 Informatics & Mathematical Modelling mailto:nielson-hAEytp/1A71/SzgSGea1oA@xxxxxxxxxxxxxxxx The Technical University of Denmark http://www.imm.dtu.dk/~nielson ----------------------------------------------------------------------