US-France (INRIA) Cooperative Research:  Type Theory and    Interactive Development of Proofs and Programs
{'Code': '01090000', 'Directorate': {'Abbreviation': 'O/D', 'LongName': 'Office Of The Director'}, 'Division': {'Abbreviation': 'OISE', 'LongName': 'Office Of Internatl Science &Engineering'}}
{'SignBlockName': 'Pierre Perrolle', 'PO_EMAI': None, 'PO_PHON': None}
This award will support a group research effort in computer science             to be carried out by researchers based at the University of                     Pennsylvania, Stanford University and Cornell University in                     collaboration with the French National Institute for Information                Science and Automation (INRIA) and the Ecole Normale Superieure,                Paris.  The U.S. group will be led by Dr. Carl Gunter and Dr. Val               Breazu-Tannen, University of Pennsylvania.  On the French side the              project will be led by Dr. Thierry Coquand, INRIA Rocquencourt.                                                                                                 The three year program of joint visits and workshops will focus on              the theory and applications of type systems.  This group of U.S.                researchers and their French counterparts have produced important               results at the interface between the theory of programming, logic               and algebra.  Researchers are presently witnessing a convergence                between logic, mathematics and computer science, in which, for                  example, deep connections between types, proofs and programs are                being discovered.  However, much remains to be done and discoveries             of further connections and parallels are anticipated.  As in any                other rapidly advancing field, many alternative systems and models              are being investigated, whose interrelationships are only partly                understood.  Improved collaboration between some of the foremost                U.S. and French researchers in this area is likely to lead to                   important results in the classification and unification of those                alternatives.  Improved semantic models supporting the combination              of parametric polymorphism and type inheritance would be of                     particular interest to the development of semantically more                     coherent object-oriented programming languages, a question of                   undoubted interest for software engineers.  In a different area,                the interaction between U.S. work on higher-order logic programming             and French work on logic-based language definition systems promises             to be very productive and lead to better prototyping environments               for program-proving and language-definition systems.
[{'FirstName': 'Carl', 'LastName': 'Gunter', 'PI_MID_INIT': 'A', 'PI_SUFX_NAME': None, 'PI_FULL_NAME': 'Carl A Gunter', 'EmailAddress': 'cgunter@uiuc.edu', 'NSF_ID': '000361179', 'StartDate': '05/01/1989', 'EndDate': None, 'RoleCode': 'Principal Investigator'}, {'FirstName': 'Val', 'LastName': 'Tannen', 'PI_MID_INIT': None, 'PI_SUFX_NAME': None, 'PI_FULL_NAME': 'Val Tannen', 'EmailAddress': 'val@cis.upenn.edu', 'NSF_ID': '000186637', 'StartDate': '05/01/1989', 'EndDate': None, 'RoleCode': 'Co-Principal Investigator'}]
{'Name': 'University of Pennsylvania', 'CityName': 'PHILADELPHIA', 'ZipCode': '191046205', 'PhoneNumber': '2158987293', 'StreetAddress': '3451 WALNUT ST STE 440A', 'StreetAddress2': None, 'CountryName': 'United States', 'StateName': 'Pennsylvania', 'StateCode': 'PA', 'CONGRESSDISTRICT': '03', 'CONGRESS_DISTRICT_ORG': 'PA03', 'ORG_UEI_NUM': 'GM1XX56LEP58', 'ORG_LGL_BUS_NAME': 'TRUSTEES OF THE UNIVERSITY OF PENNSYLVANIA, THE', 'ORG_PRNT_UEI_NUM': 'GM1XX56LEP58'}
{'Name': None, 'CityName': None, 'StateCode': None, 'ZipCode': None, 'StreetAddress': None, 'CountryCode': None, 'CountryName': None, 'StateName': None, 'CountryFlag': None, 'CONGRESSDISTRICT': None, 'CONGRESS_DISTRICT_PERF': '""'}
[{'Code': '5918', 'Text': 'FRANCE'}, {'Code': '9145', 'Text': 'SPECIAL PROGRAMS-RESERVE'}]
{'url': 'https://www.nsf.gov/awardsearch/download?DownloadFileName=1988&All=true', 'xml': '8819598.xml'}