O INESC TEC abre concurso, até 8 de janeiro de 2021 para a atribuição de uma Bolsa de Investigação (BI) no âmbito do projeto KLEE, financiado pelo Fundo Europeu de Desenvolvimento Regional (FEDER) através do Programa Operacional Competitividade e Internacionalização – COMPETE 2020 e por Fundos Nacionais através da FCT – Fundação para a Ciência e a Tecnologia, I.P. no âmbito do PTDC/CCI-COM/30947/2017 (POCI-01-0145-FEDER-030947)

1. CARACTERIZAÇÃO DA BOLSA

Tipo de bolsa: Bolsa de Investigação (BI)

Área científica genérica: COMPUTER SCIENCE

Área científica específica:

Duração da(s) bolsa(s): 4 meses, com início previsto para 2021-02-01, eventualmente renovável até fim do projeto.

Orientador científico: Renato Jorge Neves

Local da atividade de investigação: INESC TEC, Braga, Portugal

Valor da bolsa: € 805,98, conforme Tabela de Subsídios Mensais de Manutenção das bolsas financiadas pela FCT, pago por transferência bancária, podendo o bolseiro auferir remunerações adicionais, na sequência de um processo de avaliação trimestral (Artºs 19, 21º e 22º do regulamento de Bolsas do INESC TEC e anexo II), até um limite máximo de 50% do valor mensal da bolsa. O INESC TEC suporta os custos com matrícula, inscrição ou propinas, diretamente ou mediante reembolso, durante o período da bolsa.
O bolseiro beneficiará de um seguro de saúde, suportado pelo INESC TEC.

2. OBJETIVOS DA BOLSA:
O objectivo desta bolsa é implementar em Agda uma linguagem de programação baseada em componentes com latências, juntamente com semântica operacional e denotacional e um resultado de “soundness/adequacy” correspondente. Neste contexto, o termo ‘latência’ refere-se ao facto de os componentes não produzirem resultados de forma instantânea, i.e. de haver um atraso entre a recepção de dados para processamento e o envio de dados processados. Estes atrasos podem ser codificados através de uma mónada específica chamada ‘mónada das latências’. Esta mónada é particularmente relevante para a programação baseada em componentes, porque estes muitas vezes estão situados em locais diferentes, o que inevitavelmente causa atrasos nas comunicações. De um ponto de vista mais teórico, a mónada das latências tem não só uma teoria algébrica simples como também é fácil de a combinar com outras mónadas. Isso torna-a um candidato ideal para estudar “soundness/adequacy” no contexto da programação baseada em componentes; e depois extrapolar as lições aprendidas para o nível de abstração de uma mónada arbitrária.

3. SÍNTESE DO PLANO DE TRABALHOS E DE FORMAÇÃO:
Este trabalho exige algum conhecimento sobre mónadas e teoria das categorias. Também requer familiaridade
com técnicas de prova para estabelecer “soundness/adequacy”. Os primeiros dois meses do projecto serão, portanto, dedicados ao estudo destes tópicos. A próxima etapa será considerar uma linguagem de programação para componentes com latências. Como este projecto tem uma duração relativamente curta, adoptaremos uma linguagem de primeira ordem, porque “soundness/adequacy” é frequentemente mais fácil de provar neste contexto. Uma semântica para a linguagem será então fornecida através de receitas categóricas gerais. Iremos alocar dois meses para implementar a linguagem referida e respectiva semântica em Agda. O tempo restante será dedicado a provar em Agda “soundness/adequacy” para a linguagem. Ao longo do projecto iremos também desenvolver e estudar uma colecção de casos-de-estudo para ilustrar não só os resultados obtidos mas também para justificar escolhas realizadas ao longo do trabalho. Para cada etapa do projeto, iremos escrever um relatório que sumaria as lições aprendidas e os resultados obtidos. No final do projecto, estes relatórios serão compilados numa dissertação de mestrado.

4. PERFIL REQUERIDO:
Requisitos de admissão:
Licenciatura na área de Engenharia Informática/Ciências da Computação
A atribuição da bolsa pressupõe que o candidato é estudante de um ciclo de estudos ou de um curso não conferente de grau, lecionado numa Instituição de Ensino Superior.

Fatores de preferência:
– Conhecimento básico sobre teoria das categorias e mónadas – Experiência em Haskell e Agda.

Requisitos mínimos:
aluno de mestrado num curso de Engenharia Informática/Ciências da Computação

5. PROCESSO DE AVALIAÇÃO E SELEÇÃO:
Métodos de seleção e respectiva valoração: primeira fase constituída por Avaliação Curricular (AC) baseada nos critérios referidos no Art.º 12º do Regulamento de Bolsas do INESC TEC e segunda fase constituída por uma Entrevista Individual (EI). Todos os parâmetros são avaliados na escala de 0 a 100, tendo em conta o mérito, a adequação e os fatores de preferência.
Os parâmetros da AC e respetivos pesos são: Formação Académica (FA, 50%), Publicações Científicas (PC, 15%), Experiência (EX, 15%) e Carta de Motivação (CM, 20%). Os candidatos com AC < 50 são excluídos em mérito absoluto. Os melhores cinco candidatos que não sejam excluídos em mérito absoluto são chamados para a EI. A Classificação Final (CF) é obtida a partir da AC (80%) e da EI (20%).

Composição do Júri de Selecção:
Presidente do júri: Luís Soares Barbosa
Vogal: Renato Jorge Neves
Vogal: José Paiva Proença
Suplente: José Nuno Oliveira
Notificação dos resultados: os resultados do processo de seleção, bem como os prazos e procedimentos de audiência prévia, serão divulgados aos interessados por correio eletrónico, nos termos referidos no Art.º 13º do Regulamento de Bolsas do INESC TEC.

6. FORMALIZAÇÃO DAS CANDIDATURAS:
Documentos de Candidatura:
1. Carta de motivação;
2. Curriculum Vitae (deve incluir a lista de eventuais bolsas anteriores, com natureza da bolsa, datas de início e fim e instituições outorgante e de acolhimento);
3. Certificado de habilitações com o respetivo grau académico reconhecido em Portugal;
l Os documentos comprovativos da titularidade de grau académico e diploma, ou do respetivo reconhecimento, quando de trate de grau académico ou diploma atribuído por instituição de ensino superior estrangeira, podem ser dispensados em fase de candidatura, sendo substituídos por declaração de honra do candidato de acordo com minuta própria, ocorrendo a verificação daqueles apenas em fase de contratualização da bolsa. A apresentação do certificado é obrigatória para a assinatura do contrato.
l Os graus académicos ou diplomas atribuídos por instituição de ensino superior estrangeira necessitam de reconhecimento por uma instituição de ensino superior portuguesa e do respetivo registo na Plataforma da DGES, de acordo com o Decreto-lei nº. 66/2018, de 16 de agosto e a Portaria nº. 33/2019, de 25 de janeiro. Mais informação poderá ser obtida em: https://www.dges.gov.pt/pt/pagina/reconhecimento?plid=374
4. Comprovativo de inscrição em ciclo de estudos conferente de grau académico ou em curso do Ensino Superior
não conferente de grau académico.
l O comprovativo de inscrição pode ser entregue apenas em fase de contratualização da bolsa.
5. Declaração de não incumprimento dos deveres do bolseiro.
6. No caso de o bolseiro ser estrangeiro ou não residente em Portugal, deverá apresentar documento que comprove o país de residência, autorização de residência ou outro documento legalmente equivalente, com validade à data de início da bolsa.
7. Outros documentos comprovativos relevantes para a apreciação final.
A não entrega da documentação exigida, no prazo de 90 dias de calendário após a data da comunicação da
concessão condicional da bolsa, implica a caducidade da referida concessão.

Período de candidatura: De 2020-12-23 a 2021-01-08
Submissão de candidaturas: Preenchimento de formulário eletrónico em www.inesctec.pt na secção JUNTE-SE A NÓS

7. LEGISLAÇÃO E REGULAMENTAÇÃO APLICÁVEL
A contratação será regida pelo estipulado na legislação em vigor relativa ao Estatuto do Bolseiro de Investigação,
aprovado pela Lei n.º 40/2004 de 18 de agosto, na sua redação em vigor, bem como pelo Regulamento de Bolsas
do INESC TEC e pelo Regulamento de Bolsas de Investigação da FCT em vigor.
Para mais informações, consultar o Regulamento de Bolsas do INESC TEC e respetivos anexos em
www.inesctec.pt/bolsas