[TYPES/announce] Postdoc Position Reminder

[Mislove, Michael W]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear All,

This is a reminder that we have an open postdoc position in Quantum Programming 
Languages here at Tulane. The project goal is to devise models of high-level 
functional quantum programming languages that support recursion, including 
recursive types. We’re also interested in contextuality as a quantum resource. 
This is a part of a multi-university research project that includes a new team 
at the University of Maryland whose work on Hoare logics for quantum 
programming languages also is of interest. Details and application instructions 
can be found at https://apply.interfolio.com/56794 

  Thanks,
  Mike Mislove

===
Michael MislovePhone: +1 504 865-5803 

Professor and Chair FAX: +1 504 865-5063 

Department of Computer Science
Tulane University   URL: http://www.cs.tulane.edu/~mwm 

New Orleans, LA 70118 USA
===



smime.p7s
Description: S/MIME cryptographic signature

[TYPES/announce] Quantum Computation Postdoc at Tulane

[Mislove, Michael W]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Applications are invited for postdoctoral position in the Tulane Computer 
Science department. The position is part of the on-going MURI project, 
“Semantics and Tools for High-level Functional Quantum Programming Languages” 
whose focus is on developing semantic models and tools to support high-level 
quantum functional programming languages. A prototype is Proto-Quipper 
((http://www.mathstat.dal.ca/~selinger/quipper/  ). Proto-Quipper and its 
dialects use the circuit model for quantum computation that follows the 
“quantum computation under classical control” paradigm. The goal is type-safe 
functional programming languages for quantum computing. The project also 
involves developing the meta-theory (including categorical semantics) of such 
languages, and formalizing some of the meta-theory in a proof assistant. The 
focus of the Tulane work has been adding recursion to models for these 
languages. Our work has been based on the linear/nonlinear models first devised 
by Benton for linear logic, from which the ingredients needed to model circuit 
description languages have been extracted. We currently have a model for term 
recursion, and a model supporting recursive intuitionistic types is nearing 
completion. The next goals include adding dynamic lifting and developing 
concrete models based on C*- and W*-algebras, and operator systems, more 
generally. An additional component of the work is to investigate contextuality 
as a resource for demonstrating quantum advantage. Although the position is 
based at Tulane, project members may travel to the other sites where work on 
this project is taking place. These include UPenn, UIowa, UMd and Stanford in 
the US, and McGill University and Dalhousie University in Canada and Oxford and 
Edinburgh in the UK. Funding for the project comes from the DOD and the U.S. 
Air Force Office of Scientific Research.

Candidates can find more details at the application site, which can be found 
here:  https://apply.interfolio.com/56794 
/
The start date for the position is January, 2019, or as soon thereafter as 
possible. The project runs run through November 30, 2020.
Review of applications will continue until the position is filled, but to 
receive full consideration, applications should be received by December 1st.

Equal Employment Opportunity Statement
Tulane University is an Equal Employment Opportunity/Affirmative Action 
institution committed to excellence through diversity. Tulane University will 
not discriminate based upon race, ethnicity, color, sex, religion, national 
origin, age, disability, genetic information, sexual orientation, gender 
identity or expression, pregnancy, marital status, military or veteran status, 
or any other status or classification protected by federal, state, or local 
law. All eligible candidates are encouraged to apply.

[TYPES/announce] Postdoctoral Position - Error in Embedded Link

[Mislove, Michael W]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear All,
There was an error in the embedded link in the announcement I sent about the 
postdoctoral fellowship that’s open here. The corrected link is:
 https://apply.interfolio.com/41053    
Apologies for the error.
   Best regards,
   Mike Mislove

===
Michael MislovePhone: +1 504 865-5803 

Professor and Chair FAX: +1 504 865-5063 

Department of Computer Science
Tulane University   URL: http://www.cs.tulane.edu/~mwm 

New Orleans, LA 70118 USA
===



smime.p7s
Description: S/MIME cryptographic signature

[TYPES/announce] Postdoctoral Position

[Mislove, Michael W]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear All,
Below is an announcement of a postdoctoral research position starting October 1 
and running through November 30, 2018. I encourage all interested parties to 
apply. 
   Thanks,
   Mike Mislove


===
Michael MislovePhone: +1 504 865-5803 

Professor and Chair FAX: +1 504 865-5063 

Department of Computer Science
Tulane University   URL: http://www.cs.tulane.edu/~mwm 

New Orleans, LA 70118 USA
===


Postdoctoral Researcher in Semantics and Tools for Quantum Programming Languages

Applications are invited for a postdoctoral position beginning October 1, 2017 
and running through November 30, 2018. The position is in the Department of 
Computer Science at Tulane University, and will be under the supervision of 
Professor Michael Mislove. 

The successful applicant will work on a project entitled "Semantics, Formal 
Reasoning, and Tool Support for Quantum Programming”. The project involves 
designing high-level semantic models and tools to support quantum functional 
programming languages. A prototype language is Proto-Quipper, which has been  
under development (http://www.mathstat.dal.ca/~selinger/quipper/ 
 ). This language uses the 
circuit model for quantum computation, and envisions languages that support 
quantum computation under classical control. The overall aim is to design 
type-safe functional programming languages for quantum computing. The project 
also involves developing the meta-theory (including categorical semantics) of 
such languages, and eventually to formalize some of the meta-theory in a proof 
assistant. The focus of the Tulane work is modeling recursion in such 
languages, which requires developing quantum domain theory, but interactions 
with other aspects of the project are expected. 

Familiarity with programming language design, and / or semantics is a 
prerequisite of the position. The latter includes categorical semantics and 
domain theory. A good knowledge of category theory is also a prerequisite. Of 
course, familiarity with quantum computing is helpful. Additional components of 
the project will address issues around quantum information such as non-locality 
and contextuality, adapting proof assistants (Coq, Agda, Lean, etc) to develop 
automated verification for quantum programming languages. 

To apply for one of this position, direct your browser to the link: 
https://apply.interfolio.com/41053 

Funding for the project comes from the DOD and the U.S. Air Force Office of 
Scientific Research. 

smime.p7s
Description: S/MIME cryptographic signature

[TYPES/announce] Postdoctoral Position Closing

[Mislove, Michael W]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear All,
This is a reminder that the closing date for the postdoctoral position listed 
below is April 30.
  Thanks,
  Mike Mislove

===
Michael MislovePhone: +1 504 
865-5803
Professor and Chair FAX: +1 504 
865-5063
Department of Computer Science
Tulane University   URL: http://www.cs.tulane.edu/~mwm
New Orleans, LA 70118 USA
===

Postdoctoral Researcher in Semantics and Tools for Quantum Programming Languages

Applications are invited for a postdoctoral position beginning July 1 and 
running through November 30, 2018. There is a possibility of an extension 
beyond November, 2018, depending on funding. The position is
in the Department of Computer Science at Tulane University, and will be under 
the supervision of Professor Michael Mislove.

The successful applicant will work on a project entitled "Semantics, Formal 
Reasoning, and Tool Support for Quantum Programming”. The project involves 
designing high-level semantic models and tools to support
quantum functional programming languages. A prototype language is 
Proto-Quipper, which has been under development 
(http://www.mathstat.dal.ca/~selinger/quipper/ ). This language uses the 
circuit model for quantum computation, and envisions languages that support 
quantum computation under classical control. The overall aim is to design 
type-safe functional programming languages for quantum computing. The project 
also involves developing the meta-theory (including categorical semantics) of 
such languages, and eventually to formalize some of the meta-theory in a proof 
assistant. The focus of the Tulane work is modeling recursion in such 
languages, which requires developing quantum domain theory, but interactions 
with other aspects of
the project are expected.

Familiarity with programming language design, and / or semantics is a 
prerequisite of the position. The latter includes categorical semantics and 
domain theory. A good knowledge of category theory is also a
prerequisite. Of course, familiarity with quantum computing is helpful. 
Additional components of the project will address issues around quantum 
information such as non-locality and contextuality, adapting proof assistants 
(Coq, Agda, Lean, etc) to develop automated verification for quantum 
programming languages, and developing quantum routers.

Although the position is at Tulane University, candidates may travel to the 
other sites where work on this project is taking place. These include UPenn, 
UIowa and Stanford in the US, as well as McGill
University and Dalhousie University in Canada and Oxford and Edinburgh in the 
UK.

To apply for this position, direct your browser to the link: 
https://apply.interfolio.com/41053

Tulane University is an equal employment opportunity/affirmative action/persons 
with disabilities/veterans employer committed to excellence through diversity. 
Tulane will not discriminate against individuals with disabilities or veterans. 
All eligible candidates are encouraged to apply.

Funding for the project comes from the DOD and the U.S. Air Force Office of 
Scientific Research.

[TYPES/announce] Postdoc in Semantics and Tools for Functional Quantum Programming Languages

[Mislove, Michael W]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear All,
Below is an announcement for a postdoctoral position working on the MURI 
project on Semantics and Tools for Functional Quantum Programming Languages. I 
invite applications from interested candidates.
   Thanks,
   Mike Mislove

===
Michael MislovePhone: +1 504 
865-5803
Professor and Chair FAX: +1 504 
865-5063
Department of Computer Science
Tulane University   URL: http://www.cs.tulane.edu/~mwm
New Orleans, LA 70118 USA
===


Postdoctoral Researcher in Semantics and Tools for Quantum Programming Languages


Applications are invited for a postdoctoral position beginning July 1 and 
running through November 30, 2018. There is a possibility of an extension 
beyond November, 2018, depending on funding. The position is in the Department 
of Computer Science at Tulane University, and will be under the supervision of 
Professor Michael Mislove.


The successful applicant will work on a project entitled "Semantics, Formal 
Reasoning, and Tool Support for Quantum Programming”. The project involves 
designing high-level semantic models and tools to support quantum functional 
programming languages. A prototype language is Proto-Quipper, which has been  
under development (http://www.mathstat.dal.ca/~selinger/quipper/ ). This 
language uses the circuit model for quantum computation, and envisions 
languages that support quantum computation under classical control. The overall 
aim is to design type-safe functional programming languages for quantum 
computing. The project also involves developing the meta-theory (including 
categorical semantics) of such languages, and eventually to formalize some of 
the meta-theory in a proof assistant. The focus of the Tulane work is modeling 
recursion in such languages, which requires developing quantum domain theory, 
but interactions with other aspects of the project are expected.


Familiarity with programming language design, and / or semantics is a 
prerequisite of the position. The latter includes categorical semantics and 
domain theory. A good knowledge of category theory is also a prerequisite. Of 
course, familiarity with quantum computing is helpful. Additional components of 
the project will address issues around quantum information such as non-locality 
and contextuality,

adapting proof assistants (Coq, Agda, Lean, etc) to develop automated 
verification for quantum programming languages, and developing quantum routers.


Although the position is at Tulane University, candidates may travel to the 
other sites where work on this project is taking place. These include UPenn, 
UIowa and Stanford in the US, as well as McGill University and Dalhousie 
University in Canada and Oxford and Edinburgh

in the UK.


To apply for this position, direct your browser to the link: 
https://apply.interfolio.com/41053

Funding for the project comes from the DOD and the U.S. Air Force Office of 
Scientific Research.

[TYPES/announce] Postdocs at Tulane

[Mislove, Michael W]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear Colleagues,

This is a reminder that there are two postdoc positions for which I am 
currently accepting applications - the deadline to apply is February 20. The 
project is entitled, "Semantics, Formal Reasoning, and Tool Support for Quantum 
Programming”, and the focus of the work at Tulane is on developing a quantum 
domain theory.  Details can be found at the application site  
apply.interfolio.com/33550

Tulane University is an Affirmative Action / Equal Opportunity / ADA Employer 
that is committed to increasing the diversity of its faculty. We therefore 
encourage applications from underrepresented groups.

I also welcome inquiries about these positions or about the project.

 Thanks,
 Mike Mislove
 Departments of Computer Science and Mathematics
 Tulane University


===
Michael MislovePhone: +1 504 
865-5803
Professor and Chair FAX: +1 504 
865-5063
Department of Computer Science
Tulane University   URL: http://www.cs.tulane.edu/~mwm
New Orleans, LA 70118 USA
===

[TYPES/announce] Postdocs at Tulane on Semantics of Quantum Programming Languages

[Mislove, Michael W]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear Colleagues,

I invite applications for two postdoctoral positions, starting this spring or 
summer, at 
Tulane University under my supervision.

The successful applicants will work on a project entitled "Semantics, Formal 
Reasoning, and Tool Support for Quantum Programming”. The project involves 
designing high-level semantic models and tools to support quantum functional 
programming languages. A prototype language is Quipper, which currently is 
an EDSL of Haskell (http://www.mathstat.dal.ca/~selinger/quipper/ ). One goal 
is to
free Quipper from the constraints of the Haskell type system and to devise a 
type 
system tailored to the needs of quantum programming languages. The overall aim 
is to design type-safe functional programming languages for quantum computing. 
The 
project also involves developing the meta-theory (including categorical 
semantics)
of the language, and eventually the formalization of some of this meta-theory 
in a proof 
assistant. 

The focus of the Tulane work is on modeling recursion in such languages, which 
requires developing quantum domain theory. Interactions with other aspects
of the project also is expected. 

Familiarity with programming language design, and / or semantics is a 
prerequisite
for these postdocs. The latter includes categorical semantics and domain 
theory.  
Familiarity with quantum computing also is helpful, but not necessary nor 
sufficient 
for these positions. The main focus of the Tulane component of the work is on 
the semantics of quantum functional programming languages. 

Although the positions will be based at Tulane University, candidates should 
expect to travel to the 
other sites where work on this project is taking place. These include UPenn, 
UIowa and Stanford in
the US, as well as McGill University and Dalhousie University in Canada and 
Oxford and Edinburgh 
in the UK. 

Funding for the project comes from the DOD and the U.S. Air Force Office of 
Scientific Research. 
These postdocs are for a period of 3 years each. 

To apply for one of these positions, direct your browser to the link: 
apply.interfolio.com/33550 

Tulane University is an Affirmative Action / Equal Opportunity / ADA Employer 
that is committed 
to increasing the diversity of its faculty. We therefore encourage applications 
from underrepresented 
groups.

I also welcome any inquiries about these positions or about the project. 
  Thanks, 
  Mike Mislove, 
  Departments of Computer Science and Mathematics
  Tulane University