[TYPES/announce] Postdoctoral Opening at the University of Minnesota
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Applications are invited for a one-year postdoctoral position at the University of Minnesota. The position is available immediately; applications will be reviewed as they are received. The project within which the appointment is to be made concerns the development of a framework that supports the encoding of rule-based relational specifications and the process of reasoning about such specifications through the encoding. An emphasis in the project is the use of the so-called higher-order abstract syntax approach to representing objects that embody a binding structure. In recent work, we have developed a new logic <https://arxiv.org/abs/2107.00111> for articulating properties of LF specifications, which has provided the basis for a proof assistant called Adelfa <http://adelfa.cs.umn.edu> for reasoning about such properties. In other work, we are developing the capability to reason about linear logic specifications within the Abella proof assistant <https://abella-prover.org/> and are also using this system to explore the benefits of higher-order representations of syntax in the verification of compilers and transformers for functional programming languages. The successful candidate will be expected to participate in and help lead the work in some of these directions. To be suitable for the position, the candidate should be broadly conversant with the areas of computational logic and programming languages and should have the mathematical and programming skills necessary for conducting research in them. Some particular facets that would be helpful in engaging immediately with the research problems are a prior exposure to a proof assistant or logical framework such as Coq, Isabelle or Abella, programming experience with a functional language such as OCaml, an understanding of proof theoretic treatments of aspects such as fixed-point definitions, and familiarity with issues related to proof search in sequent calculi and similar logical systems. Please feel free to contact me (Gopalan Nadathur, ngopa...@umn.edu) for more details about the position. To view the official announcement, please visit the URL https://hr.myu.umn.edu/jobs/ext/330828. This site also provides details about how to apply and serves as the portal for applications. A prerequisite for employment in this capacity is a doctoral degree in Computer Science or closely related field. -Gopalan
[TYPES/announce] Postdoctoral Opening at the University of Minnesota
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Applications are invited for a one-year postdoctoral position at the University of Minnesota related to an NSF-funded project entitled "A Higher-Order Framework for Meta-Theoretic Reasoning." The position is available immediately and reviews of applications will be conducted as they are received. The project within which the appointment is to be made concerns the development of a framework that supports the encoding of rule-based relational specifications and the process of reasoning about such specifications through the encoding. A defining characteristic of the project is its focus on the so-called higher-order abstract syntax approach to representing objects that embody a binding structure. Ongoing work is aimed at developing systems for reasoning about specifications encoded in linear logic as well as in the dependently typed lambda calculus LF. The group is also interested in furthering its earlier work that has demonstrated the benefits of higher-order representations of syntax in the verification of compilers and transformers for functional programming languages. Another direction of investigation is that of enhancing the logic underlying the Abella proof assistant (see http://abella-prover.org) with the capability of predicate quantification and on exhibiting the usefulness of such an enhancement through a collection of targeted reasoning applications. The successful candidate will be expected to participate in and help lead the work in some of these directions. To be suitable for the position, the candidate should be broadly conversant with the areas of computational logic and programming languages and should have the mathematical and programming skills necessary for conducting research in them. Some particular facets that would be help in engaging immediately with the research problems are a prior exposure to a proof assistant or logical framework such as Coq, Isabelle or Abella, programming experience with a functional language such as OCaml, an understanding of proof theoretic treatments of aspects such as induction and co-induction, and familiarity with issues related to proof search in sequent calculi and similar logical systems. Please feel free to contact me (Gopalan Nadathur, ngopa...@umn.edu) for more details about the topics of research within the project, the necessary background and other relevant details about the position. To view the official announcement, please visit the URL https://hr.myu.umn.edu/jobs/ext/330828. This site also provides details about how to apply and serves as the portal for applications. The application process will require you to submit a letter indicating your interest, a current CV, one or two of your papers broadly related to the topics of research and the names and contact details for two references who might be contacted as part of the application review process. Note that a prerequisite for employment is a doctoral degree in Computer Science or closely related field. -Gopalan Nadathur
[TYPES/announce] postdoctoral opening at the University of Minnesota
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Postdoctoral Opportunity at the University of Minnesota Applications are invited for a postdoctoral position at the University of Minnesota related to an NSF-funded project entitled "A Higher-Order Framework for Meta-Theoretic Reasoning." The position is available immediately and is expected to be of duration of one to two years. Applications will be reviewed and acted upon as soon as they are received. The project within which the appointment is to be made concerns the further development of a proof environment for reasoning about relational specifications that supports the so-called higher-order abstract syntax approach. A key component of this environment is the Abella proof assistant (see http://abella-prover.org), which is based on a logic that incorporates a treatment of fixed-point definitions. One thrust for ongoing work is the enhancement of the underlying logic, for example through the addition of predicate quantification. The research group is also interested in building into the Abella system the capability to reason about specifications written in linear logic and dependently typed lambda calculi, and in investigating the benefits of the system in tasks such as compiler verification. To participate successfully in the research described above, you would need to be broadly conversant with the areas of computational logic and programming languages and to have the mathematical and programming skills necessary for conducting original work in these areas. Prior exposure to a proof assistant or logical framework such as Coq, Isabelle or Abella, programming experience with a functional language such as OCaml, an understanding of proof theoretic treatments of aspects such as induction and co-induction, and familiarity with issues related to proof search in sequent calculi and other similar logical systems would help in engaging immediately with the research problems of interest. To view the official announcement for this position, please visit the URL https://hr.myu.umn.edu/jobs/ext/330828. This site also provides details such as the required qualifications for the position and serves as the portal for applications. To complete an application, you would need to submit a letter indicating your interest in the position, a current CV, one or two papers broadly related to the topics of research and the names and contact details of two people who are willing to serve as your references in the review process. Please do not hesitate to contact me if you have an interested in the position but would like answers prior to applying to questions related to matters such as the expectations, possible projects, and the suitability of your qualifications for the position. The best way to reach me would be via email sent to ngopa...@umn.edu. -Gopalan Nadathur
[TYPES/announce] postdoctoral opening at the University of Minnesota
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Applications are invited for a one-year postdoctoral position, possibly extendable into a second year, at the University of Minnesota related to an NSF-funded project entitled "A Higher-Order Framework for Meta-Theoretic Reasoning." The position is available immediately and reviews of applications will be conducted as they are received. The project within which the appointment is to be made concerns the further development of a logic that incorporates a treatment of fixed-point definitions and the enhancement of the capabilities of the Abella proof assistant (see http:\\abella-prover.org) that is based on this logic. One particular extension to the underlying logic that is being investigated is the addition of predicate quantification. The research group is also interested in building into the Abella system the capability to reason about specifications written in linear logic and dependently typed lambda calculi, and in demonstrating the benefits of the system in tasks such as compiler verification. To be suitable for the position, the candidate should be broadly conversant with the areas of computational logic and programming languages and should have the mathematical and programming skills necessary for conducting research in them. Prior exposure to a proof assistant or logical framework such as Coq, Isabelle or Abella, programming experience with a functional language such as OCaml, an understanding of proof theoretic treatments of aspects such as induction and co-induction, and familiarity with issues related to proof search in sequent calculi and other similar logical systems would be needed for participating in the research at the appropriate level. For more details about the necessary background and possible topics of research within the project, please feel free to contact me (Gopalan Nadathur) via email at ngopa...@umn.edu. To view the official announcement for this position, please visit the URL https://hr.myu.umn.edu/jobs/ext/330828. This link also provides details about how to apply and serves as the portal for applications. The application process will require you to submit a letter indicating your interest, a current CV, one or two of your papers broadly related to the topics of research and the names and contact details for two references who might be contacted as part of the application review process. Note that a prerequisite for employment is a doctoral degree in Computer Science or closely related field.
[TYPES/announce] Special Issue of MSCS---Call for Papers
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Call for Papers Special Issue of Mathematical Structures in Computer Science in Celebration of the Sixtieth Birthday of Dale Miller Papers are invited to a special issue of Mathematical Structures in Computer Science, a journal published by Cambridge University Press. This special issue is being collated in celebration of the sixtieth birthday of Professor Dale Miller. To be appropriate for this collection, papers must be broadly related to one or more of the areas that have been spanned by the work of Professor Miller to-date. These areas include structural proof theory, proof search and computation, foundations of logic programming, higher-order unification, reasoning about relational specifications and certification of proofs. This list is meant to be illustrative and is not exhaustive; if you are interested in submitting a paper and would like to ascertain its relevance to the theme of the special issue, please feel free to contact the editors of the issue. Papers that are submitted for consideration of publication must be prepared in LaTeX and should use the MSCS style file that can be downloaded from ftp.cup.cam.ac.uk. Please also follow the layout and other manuscript format related instructions with the exception of double spacing that you will find at http://z.umn.edu/mscsformat. Manuscripts should also be limited to about 25 pages. While this is not a hard constraint, the reason why a paper exceeds this limit must be apparent to the editors from an inspection of its content, else it may be declined without review. To ensure timeliness of publication, strict deadlines and an expedited reviewing process will be followed in the preparation of this special issue. To be considered for publication, manuscripts must be submitted by May 31, 2017. The first round of reviews will be completed by July 31, 2017. Revised versions of manuscripts that are deemed to be of acceptable quality will be due by August 21, 2017 and final acceptance decisions will be made by September 11, 2017. To submit a manuscript to the special issue, please use the ScholarOne site for MSCS at https://mc.manuscriptcentral.com/mscs. Once you are at this site, you will need to create an account if you do not have one already. Once you are logged in, select the "Author" tab and follow the instructions. At the end of the page, under the "Special Issue" heading, select "Miller Festschrift" prior to submission. Please note that at this stage we will need only a PDF file prepared as indicated above. The LaTeX source will be required after the manuscript has been accepted. Regards, David Baelde (david.bae...@lsv.ens-cachan.fr) Amy Felty (afe...@eecs.uottawa.ca) Gopalan Nadathur(gopa...@cs.umn.edu) Alexis Saurin (alexis.sau...@irif.fr)
[TYPES/announce] PhD opportunities at the Univ. of Minnesota
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Are you interested in research in programming languages and logic? Then consider applying to the graduate program in Computer Science at the University of Minnesota. There are several openings for funded doctoral research in extensible programming languages (realized in tools such as Silver, Copper, and ableC, see http://melt.cs.umn.edu) and in logics for specifying and reasoning about computational systems (see http://teyjus.cs.umn.edu/, http://abella-prover.org/, and http://sparrow.cs.umn.edu/compilation/ for some projects). There are also opportunities for collaborations in the use of formal methods in software verification both with the Software Engineering group in the department and with ones in the local industry, such as at Rockwell-Collins. Moreover, the Twin Cities (Minneapolis and St. Paul) offers an extremely livable environment with several cosmopolitan attractions: theater, restaurants, great public transportation, and varied outdoor activities both around the cities and around Lake Superior that is a short drive away. If this possibility intrigues you and you would like to get more specific information, don't hesitate to contact one of us via email. Best regards, Eric Van Wyk (e...@umn.edu) Gopalan Nadathur (gopa...@cs.umn.edu)
[TYPES/announce] Book Announcement
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dale Miller and I are happy to announce the recent publication of our book entitled Programming with Higher-Order Logic by Cambridge University Press. The table of contents and other details about the book can be found at https://sites.google.com/site/proghol/. The book argues for using higher-order intuitionistic logic as the foundations of logic programming. In elaborating this argument, the book presents - a sequent calculus based characterization of logic programming; - a proof search approach to computation; - higher-order logic programming; - polymorphic typing; - modular programming and abstract data types; and - simply-typed lambda-terms and their unification. The book also emphasizes the practical application of higher-order logic programming by showing that it can be used to provide elegant formalizations and implementations of computations that manipulate bindings in syntax. In addition to a general exposition of this approach, individual chapters present extended examples relating to - implementing proof systems, - computing with functional programs, and - encoding the pi-calculus. The lambda Prolog language is used to illustrate the underlying computation-related ideas and their applications. The website for the book provides all the lambda Prolog code used in the book. The reader can experiment with this code using the Teyjus system available from http://teyjus.cs.umn.edu/.
[TYPES/announce] Postdoctoral Position at the University of Minnesota
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Applications are invited for a one-year postdoctoral position at the University of Minnesota related to an NSF-funded project entitled Reasoning about Specifications of Computations. The position is available immediately: to guarantee consideration, applications must be received before September 7, 2012. The project within which the appointment is to be made concerns the areas of computational logic and programming languages. To be suitable for the position, the candidate should be broadly conversant with the issues in these areas and should have the mathematical and programming skills necessary for conducting research in them. Moreover, with suitable mentoring, he/she should be capable of developing an independent research agenda that encompasses some of the following topics: * the design of logics for specifying computational systems and for reasoning about such specifications, * the implementation of systems embodying such logics, and * the use of the implemented systems in constructing actual specifications and reasoning about them. Facility with proof assistants and logical frameworks such as Coq, Isabelle and Twelf, an understanding of proof theoretic treatments of aspects such as induction and co-induction and familiarity with issues related to proof search in sequent calculi and related logical systems would be needed for participating in the research at the appropriate level. A specific focus for the project is the Abella system (see http://abella.cs.umn.edu), developed originally at the University of Minnesota and currently also the subject of work within the Parsifal project at Ecole Polytechnique and INRIA, Saclay. The ideal candidate would have an interest in further developing the capabilities of this system and its applications during the appointment period. To apply for this position, go to the U of M Employment System at https://employment.umn.edu/ and search postings with req#: 179943. The online application process will require you to submit a current CV and a brief research statement that should describe past research and future plans in a way that addresses appropriateness for the position advertised. Please also provide names, phone numbers and email addresses of two or three references as part of this material; these references may be contacted as part of the application review process. Note that a prerequisite for employment is a doctoral degree in Computer Science or closely related field. Interested individuals are encouraged to contact Gopalan Nadathur at gopa...@cs.umn.edu for more information towards assessing the suitability of an application.
[TYPES/announce] LFMTP 2011 Call for Papers (2nd Call)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] [LFMTP 2011 Reminder: Abstracts due by May 16, papers due by May 23] Sixth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'11) http://lfmtp11.cs.umn.edu Nijmegen, The Netherlands, August 27, 2011 Affiliated with Interactive Theorem Proving (ITP 2011) CALL FOR PAPERS - IMPORTANT DATES Abstract submission: May 16, 2011 Paper submission:May 23, 2011 Author notification: June 22, 2011 Final versions due: August 1, 2011 Workshop day:August 27, 2011 - 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 on the one hand and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems on the other hand have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors, and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressivity and lucidity of the reasoning process. The broad subject areas of LFMTP'11 are: * Encoding and reasoning about the meta-theory of programming languages and related formally specified systems. * Theoretical and practical issues concerning the treatment of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures. * Logical treatments of inductive and co-inductive definitions and associated reasoning techniques. * Case studies of meta-programming, and the mechanization of the (meta)theory of descriptions of programming languages and other calculi. Papers focusing on logic translations and on experiences with encoding programming languages theory are particularly welcome. Submission and other details concerning the workshop can be found at its website at http://lfmtp11.cs.umn.edu.
[TYPES/announce] Postdoctoral Opportunity at the University of Minnesota
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Applications are invited for a one-year postdoctoral position at the University of Minnesota. The appointment is expected to start in Fall 2009 and will be in the areas of computational logic and programming languages. The selected candidate will be expected to conduct research on some of the following topics: * the design of logics for specifying computational systems and for reasoning about such specifications, * the implementation of systems embodying such logics, and * the use of the implemented systems in constructing actual specifications and reasoning about them. A deep understanding of proof theoretic treatments of aspects such as induction and co-induction and of issues related to proof search in sequent calculi and related logical systems is needed for participating in such research at the appropriate level. Familiarity with proof assistants and logical frameworks such as Coq and Twelf will also be beneficial. To apply for this position, go to the U of M Employment System at https://employment.umn.edu/ and search postings with req#: 162068. The online application process will require you to submit a current CV, the names and contact information of three references and a research statement of approximately two pages that describes past research and future plans in a way that addresses appropriateness for the position advertised. A prerequisite for employment is a doctoral degree in Computer Science or closely related field. Review of applications will begin by August 1, 2009 and continue until the position is filled. Questions about the position may be directed to Gopalan Nadathur at gopa...@cs.umn.edu.
