[TYPES/announce] Open positions in crypto/security at ITU
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear colleagues, The newly established Center for Information Security Research (CISR) at IT University of Copenhagen (cisr.dk <http://cisr.dk/>), is seeking applications for one or more full time faculty positions at the rank of assistant professor or associate professor in cryptography and network security. Applications in other areas of security will also be considered. https://candidate.hr-manager.net/ApplicationInit.aspx?cid=119=180959=5 <https://candidate.hr-manager.net/ApplicationInit.aspx?cid=119=180959=5> Deadline for application is June 1, 2018. The IT University is a small university with about 2600 students. Teaching load is reasonable and the salary will be in accordance with the Ministry of Finance’s agreement with the Danish Confederation of Professional Associations (AC). If you have further questions, don’t hesitate to contact us. Alessandro Bruni (b...@itu.dk <mailto:b...@itu.dk>) Rosario Giustolisi (r...@itu.dk <mailto:r...@itu.dk>) Søren Debois (deb...@itu.dk <mailto:deb...@itu.dk>) Carsten Schuermann (cars...@itu.dk <mailto:cars...@itu.dk>) Willard Rafnsson (w...@itu.dk <mailto:w...@itu.dk>) Early expression of interest is encouraged. Please re-distribute. Best regards, - Carsten Schuermann
[TYPES/announce] Open Faculty Positions at the IT University of Copenhagen
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear all, The IT University of Copenhagen (ITU) invites applications for several full-time faculty positions at the rank of assistant professor or associate professor. Among others, ITU is growing its faculty in the areas of * Security * Cryptography. We are looking for candidates with an established track record in information security, language based security, network security, or offensive security. If you are interested in contributing to building a strong security group in Copenhagen, please apply. For more information, and to file an application, please visit https://candidate.hr-manager.net/ApplicationInit.aspx?cid=119=180848=5#sthash.Tc6Owms6.dpuf <https://candidate.hr-manager.net/ApplicationInit.aspx?cid=119=180848=5#sthash.Tc6Owms6.dpuf> We look forward to hearing from you. Please circulate. Best regards, - Carsten Schuermann
[TYPES/announce] Post-Doc at IT University of Copenhagen/DemTech
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear all, The Security Group at the Department of Computer Science, IT University of Copenhagen and DemTech are looking for a two year post-doc starting 1 June 2017. The position is part of a joint project with Carnegie Mellon University (Pittsburgh, USA and Qatar) on Automated verification of properties of concurrent, distributed and parallel specifications with applications to computer security. Application deadline: 19 April 2017, at 23:59 CET (Note that this is a hard deadline) For more information: - About the project: http://www.cs.cmu.edu/~iliano/projects/metaCLF2/index.shtml - About applying: https://candidate.hr-manager.net/ApplicationInit.aspx?cid=119=180845=5#sthash.SbYYhDlJ.dpuf Or just contact me: cars...@itu.dk <mailto:cars...@itu.dk> or Iliano Cervesato: ili...@cmu.edu <mailto:ili...@cs.cmu.edu> Please distribute. Best regards, - Carsten Schuermann
[TYPES/announce] PostDoc position at ITU
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The IT University of Copenhagen seeks to hire outstanding researchers at its Interdisciplinary Centre for Democracy and Technology (DemTech). The research will be conducted under the supervision of Carsten Schuermann. DemTech specializes on mathematical foundations of secure multi-party computation, the design and analysis of cryptographic primitives and protocols, formal languages for voting systems and their properties, and automated tools to reason about them. DemTech has expertise in both the symbolic and the computational styles of protocol analysis. DemTech has established itself as a leading center for research on trust and security in election technologies. Your role is to work on the logical foundations of secure multi-party distributed systems, the modelling of voting protocols, the automated extraction of software from high-level description, and the automatic verification of security properties, both in the symbolic and the computational model. A successful applicant will hold a PhD in Computer Science or Applied Mathematics,a proven interest in reasoning systems, cryptography, or security modelling. Experience in cryptography will be considered an advantage. The appointment will will initially one year that can be extended. You will work in an exciting international setting and participate in a fast growing and dynamic research environment. For inquiries please contact, Pia Kystol Sørensen (pksr@itudk) or Carsten Schürmann (cars...@itu.dk) The position is available now.
[TYPES/announce] Two postdoctoral positions @ CMU and ITU
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [Apologies if you have received multiple copies of this announcement] === Two Postdoctoral Positions on Automated Verification of Properties of Concurrent, Distributed and Parallel Specifications Carnegie Mellon University and IT University of Copenhagen === We are seeking applications for two postdoctoral positions in computational logic. Both position are part of a common project on automated verification of properties of concurrent, distributed and parallel specifications with applications to computer security. One position is based on CMU's Qatar campus and the other in Copenhagen. Applicants should have a strong background and interest in some combination of type theory, proof theory, concurrency, logical frameworks, and linear or substructural logics. Both positions are expected to start in the Fall of 2015. Project page: http://www.cs.cmu.edu/~iliano/projects/metaCLF/ <http://www.cs.cmu.edu/~iliano/projects/metaCLF/> Application page for the position at CMU: http://csjobs.qatar.cmu.edu <http://csjobs.qatar.cmu.edu/> Application page for the position at ITU: http://en.itu.dk/About-ITU/Vacancies <http://en.itu.dk/About-ITU/Vacancies> === Iliano Cervesato Professor Carnegie Mellon University Carsten Schuermann Associate Professor IT University of Copenhagen
[TYPES/announce] Two Postdoc Positions at the IT University of Copenhagen
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The IT University of Copenhagen invites applications for several Postdoctoral fellow positions on trustworthy electronic election technology. The positions are part of the DemTech project, a larger effort to prove that it is possible to modernize the democratic process without losing the trust of the voters. We plan to use epistemic logical framework technology and cryptographic methods, such as full homomorphic encryption. The research will be conducted under the supervision of Profs. Joseph Kiniry and Carsten Schürmann. A successful applicant will be hired initially for one year with the option to renew. The start date is flexible, but the position cannot be filled before 1 July, 2011. Candidates are also encouraged to explore research ideas beyond the project description. The positions provide significant opportunities for professional development. Postdoctoral candidates should have a Ph.D. in Computer Science or Mathematics and an established research record in one or more of the following fields: applied formal methods cryptography electronic voting systems (of primary importance) rigorous software engineering trust and trustworthiness logic and semantics logical frameworks and type theory proof theory and higher-order theorem proving program verification Early expressions of interest are encouraged: Carsten Schuermann ( cars...@itu.dk), Joseph Kiniry (kin...@itu.dk). The application deadline May 15. 2011. Please follow this link Post doc in Computer Science to file your application. Best regards, -- Carsten Schuermann and Joseph Kiniry
[TYPES/announce] PhD Positions on Trustworthy Electronic Elections
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] PhD Positions on Trustworthy Electronic Elections (for more information see http://www.demtech.dk/) The IT University of Copenhagen invites applications for several PhD positions on developing and evaluating trustworthy electronic election technology. With this project, we try to prove that it is possible to modernize the democratic process using information technology without losing the trust of the voters. The PhD positions are concerned with different aspects of this research question, for example, how to design formal techniques to hold machines accountable for their actions, to run trusted code in untrusted environments, to develop software in a trust-preserving way, and to evaluate technology form a societal point of view. Applicants should have a strong background and interest in some combination of the following areas in computer science: cryptography, concurrency, epistemic logics, formal methods, information security, modal logics, operational semantics, programming languages, proof assistants, logical frameworks, requirement engineering, rewriting theory, security protocol design, software engineering, theorem proving, type theory and social science: democracy and science, democratic governance, ethnographic studies and ethnography of technologies, genealogy of democracy and technology, political technologies, public understanding of science, trust in information, science and technology studies (STS). To apply, please visit the project homepage http://www.demtech.dk/. Early expressions of interest are encouraged: Carsten Schuermann (cars...@itu.dk), Joseph Kiniry (kin...@acm.org), Randi Markussen (r...@itu.dk), Christopher Gad (c...@itu.dk), or nina Boulus (n...@itu.dk). Best regards, -- Carsten Schuermann and Joseph Kiniry
[TYPES/announce] FIRST PhD Autumn School on Modal Logic
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Call for Participation FIRST PhD Autumn School on Modal Logic IT University of Copenhagen, Denmark November 10-11 2009 http://hylocore.ruc.dk/m4m6school.html The goal of the Autumn School on Modal Logic is to prepare PhD students and other researchers for participation in the sixth workshop Methods for Modalities (M4M-6) which takes place November 12-14 2009 in Copenhagen. The workshop Methods for Modalities aims to bring together researchers interested in developing proof tools and decision methods based on modal logics. Here the term modal logics is conceived broadly, including description logic, guarded fragments, conditional logic, temporal and hybrid logic, etc. The first M4M workshop took place in Amsterdam in 1999. Since then, M4M workshops have taken place in 2001 (Amsterdam), 2003 (Nancy), 2005 (Berlin), and 2007 (Paris). See Methods for Modalities for more information on the workshop series, in particular, see why modal logic is important for computer science. A goal of having M4M in Denmark is to strengthen Danish research in reasoning methods for modal logics, which is a growing area of foundational and increasingly computational importance. The Autumn School on Modal Logic is open to anyone interested. The intended participants will have a general background in theoretical computer science, but wish to obtain more concrete knowledge on modal logic and its computational aspects. Besides a working knowledge of English, prerequisites are a basic knowledge of logic and mathematics that is usually covered in undergraduate classes on discrete mathematics. Lecturers and topics Computational Modal Logic Carlos Areces and Patrick Blackburn, INRIA, Nancy Temporal Logics for Specification and Verification Valentin Goranko, Technical University of Denmark The Judgmental Reconstruction of Modal Logic Carsten Schürmann, IT University of Copenhagen Resolution-Based Theorem Proving for Modal and Description Logic Renate Schmidt, University of Manchester Hybrid Deduction Patrick Blackburn, INRIA, Nancy For more information about the contents, see the Fall school web site: http://hylocore.ruc.dk/m4m6school.html Time and place The Fall school will take place at the IT University of Copenhagen November 10 and 11 2009. Registration The registration deadline for the Autumn school is *** Friday, October 23 2009 *** Please register here: http://hylocore.ruc.dk/m4m6registration.html FIRST PhD students participate free of charge. Organization Thomas Bolander, Technical University of Denmark Torben Braüner, Roskilde University Carsten Schürmann, IT University of Copenhagen Sponsorship The Fall school is sponsored by the FIRST Research School.
[TYPES/announce] Open PhD positions
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear colleagues, the IT University of Copenhagen (ITU) invites applications for several PhD scholarships starting in September 2009 in the following areas: Algorithms for searching and storing of large amounts of data, automated reasoning, business processes, category theory, complexity theory, concurrency theory, distributed and mobile computing, domain theory, efficient solutions to problems arising in logical formulations within planning, empirical studies of software development in organizations, scheduling, verification, test, and configuration; efficient computation, electronic health records, electronic voting, logical frameworks, software architectures, object-oriented methodology and notations, programming languages, programming language technology for functional and object-oriented languages, proof assistants, semantics, ubiquitous computing, user interface software technology, workflow languages. Applicants accepted will be employed and enrolled at the IT University for a period of 3 or 4 years. Appointment and salary will be in accordance with the agreement between the Ministry of Finance and the Danish Confederation of Professional Associations. For example, the basic salary of a 3 year PhD student amounts to DKK 24,117.18 (Euro 3236.20) per month. For more information consult the webpage: http://www1.itu.dk/sw487.asp I would be grateful if you could circulate this information among potential applicants. Best regards, -- Carsten Schuermann
[TYPES/announce] CADE-22 last call for papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] LAST CALL FOR PAPERS CADE-22 22nd International Conference on Automated Deduction McGill University, Montreal, Canada August 2-7, 2009 Submission Deadline: 23 Feb 2009 http://complogic.cs.mcgill.ca/cade22/ GENERAL INFORMATION CADE is the major forum for the presentation of research in all aspects of automated deduction. The conference programme will include invited talks, paper presentations, system descriptions, workshops, tutorials, and system competitions. SCOPE We invite high-quality submissions on the general topic of automated deduction, including foundations, applications, implementations and practical experiences. Logics of interest include, but are not limited to o propositional, first-order, equational, higher-order, classical, description, modal, temporal, many-valued, intuitionistic, other non-classical, meta-logics, logical frameworks, type theory and set theory. Methods of interest include, but are not limited to o saturation, resolution, instance-based, tableaux, sequent calculi, natural deduction, term rewriting, decision procedures, model generation, model checking, constraint solving, induction, unification, proof planning, proof checking, proof presentation and explanation. Applications of interest include, but are not limited to o program analysis and verification, hardware verification, mathematics, natural language processing, computational linguistics, knowledge representation, ontology reasoning, deductive databases, functional and logic programming, robotics, planning, and other areas of AI. INVITED SPEAKERS: Konstantin Korovin The University of Manchester Martin RinardMassachusetts Institute of Technology Mark Stickel SRI International WORKSHOPS, TUTORIALS, SYSTEM COMPETITIONS: There will be a two-day programme of eight workshops and four tutorials before the conference. In addition, two system competitions will be held during the conference. Workshops: o Automated Deduction: Decidability, Complexity, Tractability (ADDCT) o Beyond SAT: What About First-Order Logic? o Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP) o Modules and Libraries for Proof Assistants (MLPA) o Proof Search in Type Theories (PSTT) o Satisfiability Modulo Theories (SMT) o The International Workshop on Unification (UNIF) o TPTP World Workshop (TPTPWoWo) Tutorials: o Hierarchical and Modular Reasoning in Complex Theories o Probabilistic Analysis Using a Theorem Prover o Precise, Automated and Scalable Verification of Systems Software Using SMT solvers o Logics with Undefinedness System competitions: o The CADE ATP System Competition (CASC) o Satisfiability Modulo Theories Competition (SMT-COMP) Details will be published in separate calls and on the conference website. STUDENT AWARDS Travel awards will be available to enable selected students to attend the conference. Details will be published on the conference website. PUBLICATION DETAILS: The proceedings of the conference will be published in the Springer LNAI/LNCS series. SUBMISSION INSTRUCTIONS: Submissions can be made in the categories 'regular papers' and 'system descriptions'. The page limit in Springer LNCS style is 15 pages for regular papers and 5 pages for system descriptions. Full system descriptions that provide in-depth presentation of original ideas in an implemented system can be submitted as regular papers. For the benefit of reviewers, additional material may be provided by a clearly marked appendix or a reference to a manuscript on a website. It is at the discretion of the reviewers whether such supplements will be considered. All regular papers will be evaluated according to the highest standards in terms of originality, significance, technical quality, and readability. Submissions must be in English and standard conforming pdf format. Submissions must be unpublished and not submitted for publication elsewhere. Authors are strongly encouraged to produce their papers in LaTeX. Formatting instructions and the LNCS style files can be obtained via http://www.springer.de/comp/lncs/authors.html. To submit your paper please use the EasyChair submission system at this address: http://www.easychair.org/conferences/?conf=cade22. IMPORTANT DATES: A paper title and a short abstract of about 100 words must be submitted before the paper. 16 Feb 2009 Abstract submission deadline 23 Feb 2009 Paper submission deadline 10 Apr 2009 Notification of
[TYPES/announce] CADE-22 second call for papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] SECOND CALL FOR PAPERS CADE-22 22nd International Conference on Automated Deduction McGill University, Montreal, Canada August 2-7, 2009 Submission Deadline: 23 Feb 2009 http://complogic.cs.mcgill.ca/cade22/ GENERAL INFORMATION CADE is the major forum for the presentation of research in all aspects of automated deduction. The conference programme will include invited talks, paper presentations, system descriptions, workshops, tutorials, and system competitions. SCOPE We invite high-quality submissions on the general topic of automated deduction, including foundations, applications, implementations and practical experiences. Logics of interest include, but are not limited to o propositional, first-order, equational, higher-order, classical, description, modal, temporal, many-valued, intuitionistic, other non-classical, meta-logics, logical frameworks, type theory and set theory. Methods of interest include, but are not limited to o saturation, resolution, instance-based, tableaux, sequent calculi, natural deduction, term rewriting, decision procedures, model generation, model checking, constraint solving, induction, unification, proof planning, proof checking, proof presentation and explanation. Applications of interest include, but are not limited to o program analysis and verification, hardware verification, mathematics, natural language processing, computational linguistics, knowledge representation, ontology reasoning, deductive databases, functional and logic programming, robotics, planning, and other areas of AI. INVITED SPEAKERS: Konstantin Korovin The University of Manchester Martin RinardMassachusetts Institute of Technology Mark Stickel SRI International WORKSHOPS, TUTORIALS, SYSTEM COMPETITION: A two-day workshop and tutorial programme will be co-organized with the conference. In addition, the annual CADE ATP System Competition (CASC) will be held during the conference. Details will be published in separate calls and on the conference website. PUBLICATION DETAILS: The proceedings of the conference will be published in the Springer LNAI/LNCS series. SUBMISSION INSTRUCTIONS: Submissions can be made in the categories 'regular papers' and 'system descriptions'. The page limit in Springer LNCS style is 15 pages for regular papers and 5 pages for system descriptions. Full system descriptions that provide in-depth presentation of original ideas in an implemented system can be submitted as regular papers. For the benefit of reviewers, additional material may be provided by a clearly marked appendix or a reference to a manuscript on a website. It is at the discretion of the reviewers whether such supplements will be considered. All regular papers will be evaluated according to the highest standards in terms of originality, significance, technical quality, and readability. Submissions must be in English and standard conforming pdf format. Submissions must be unpublished and not submitted for publication elsewhere. Authors are strongly encouraged to produce their papers in LaTeX. Formatting instructions and the LNCS style files can be obtained via http://www.springer.de/comp/lncs/authors.html. To submit your paper please use the EasyChair submission system at this address: http://www.easychair.org/conferences/?conf=cade22. IMPORTANT DATES: A paper title and a short abstract of about 100 words must be submitted before the paper. 16 Feb 2009 Abstract submission deadline 23 Feb 2009 Paper submission deadline 10 Apr 2009 Notification of paper decisions 14 May 2009 Camera-ready papers due 2-3 Aug 2009 Workshops Tutorials 4-7 Aug 2009 Conference, including CASC PROGRAM COMMITTEE: Alessandro Armando Università di Genova Franz Baader Technische Universität Dresden Peter Baumgartner NICTA, Canberra Maria Paola Bonacina Università degli Studi di Verona Bernhard Beckert Universität Koblenz-Landau Nikolaj BjørnerMicrosoft Research Alessandro Cimatti Istituto per la Ricerca Scientifica e Tecnologica, Trento Silvio GhilardiUniversità degli Studi di Milano Jürgen Giesl RWTH Aachen Rajeev GoréThe Australian National University Reiner Hähnle Chalmers University of Technology John Harrison Intel Corporation Miki Hermann École Polytechnique Ullrich HustadtUniversity of Liverpool Katsumi Inoue National Institute of Informatics, Japan Tommi Junttila Helsinki University of Technology Deepak Kapur University of New Mexico Alexander Leitsch
[TYPES/announce] Final call: ITU PhD applications
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear all, I am writing to inform you that the IT University of Copenhagen is looking for outstanding PhD applicants in the areas of Programming languages, automated reasoning, logical frameworks, proof assistants, semantics, category theory, domain theory, distributed and mobile computing, business processes, concurrency theory, electronic voting, formal methods, verification, algorithms, planning, scheduling, verification, test, configuration; user interface software technology, ubiquitous computing, software architectures, empirical studies of software development in organizations, functional and object-oriented languages. Please find more information about the PhD positions on our webpage. http://www1.itu.dk/sw13225.asp Application deadline: October 10, 2008, noon. Sincerely yours, -- Carsten Schuermann
[TYPES/announce] Call for PhD students
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear all, I am writing to inform you that the IT University of Copenhagen is looking for outstanding PhD applicants in the areas of Programming languages, automated reasoning, logical frameworks, proof assistants, semantics, category theory, domain theory, distributed and mobile computing, business processes, concurrency theory, electronic voting, formal methods, verification, algorithms, planning, scheduling, verification, test, configuration; user interface software technology, ubiquitous computing, software architectures, empirical studies of software development in organizations, functional and object-oriented languages. Please find more information about the PhD positions on our webpage. http://www1.itu.dk/sw13225.asp Application deadline: October 10, 2008, noon. Sincerely yours, -- Carsten Schuermann
[TYPES/announce] LFMTP-07: Call for participation
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'07) 15 July, 2007 Bremen, Germany http://www.cs.mcgill.ca/~bpientka/lfmtp07/ A CADE-21 affiliated workshop http://www.cadeconference.org/meetings/cade21/ Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation has been the focus of considerable research over the last two decades, using competing and sometimes incompatible basic principles. This workshop will bring together designers, implementors, and practitioners to discuss all aspects of logical frameworks. Topics include, but are not limited to: - logical framework design - meta-theoretic analysis - applications and comparative studies - implementation techniques - efficient proof representation and validation - proof-generating decision procedures and theorem provers - proof-carrying code - substructural frameworks - semantic foundations - methods for reasoning about logics - formal digital libraries. Invited speaker: Randy Pollack. Locally Nameless Representation and Nominal Isabelle Accepted papers: Alberto Momigliano, Alan J. Martin and Amy P. Felty. Two-Level Hybrid: A System for Reasoning Using Higher-Order Abstract Syntax William Lovas and Frank Pfenning. A Bidirectional Refinement Type System for LF Paul Callaghan. Coercive Subtyping via Mappings of Reduction Behaviour Brigitte Pientka, Florent Pompigne and Xi Li. Focusing the Inverse Method for LF: a Preliminary Report Julien Narboux and Christian Urban. A Formalisation of the Logical Relation Proof given by Crary for Completeness of Equivalence Checking Alexandre Buisse and Peter Dybjer. Formalizing Categorical Models of Type Theory in Type Theory Michael Zeller, Aaron Stump and Morgan Deters. A Signature Compiler for the Edinburgh LF Anders Schack-Nielsen. Induction on Concurrent Terms Fredrik Lindblad. Higher-Order Proof Construction Based on First-Order Narrowing Murdoch Gabbay and Stephane Lengrand. The Lambda Context Calculus Registration to the LFMTP workshop is independent from registration to CADE-21. http://www.cadeconference.org/meetings/cade21/registration.html I hope to see you there, Best regards, Carsten Schuermann
