Solução rasterizada para o problema de empacotamento de fita irregular utilizando a Montanha Voronoi.

O empacotamento irregular de fita é um grupo de problemas na área de corte e empacotamento, cuja aplicação é observada nas indústrias têxtil, moveleira e construção naval. O problema consiste em definir uma configuração de itens irregulares de modo que o comprimento do contêiner retangular que contém o leiaute seja minimizado. A solução deve ser válida, isto é, não deve haver sobreposição entre os itens, que não devem extrapolar as paredes do contêiner. Devido a aspectos práticos, são admitidas até quatro orientações para o item. O volume de material desperdiçado está diretamente relacionado à qualidade do leiaute obtido e, por este motivo, uma solução eficiente pressupõe uma vantagem econômica e resulta em um menor impacto ambiental. O objetivo deste trabalho consiste na geração automática de leiautes de modo a obter níveis de compactação e tempo de processamento compatíveis com outras soluções na literatura. A fim de atingir este objetivo, são realizadas duas propostas de solução. A primeira consiste no posicionamento sequencial dos itens de modo a maximizar a ocorrência de posições de encaixe, que estão relacionadas à restrição de movimento de um item no leiaute. Em linhas gerais, várias sequências de posicionamentos são exploradas com o objetivo de encontrar a solução mais compacta. Na segunda abordagem, que consiste na principal proposta deste trabalho, métodos rasterizados são aplicados para movimentar itens de acordo com uma grade de posicionamento, admitindo sobreposição. O método é baseado na estratégia de minimização de sobreposição, cujo objetivo é a eliminação da sobreposição em um contêiner fechado. Ambos os algoritmos foram testados utilizando o mesmo conjunto de problemas de referência da literatura. Foi verificado que a primeira estratégia não foi capaz de obter soluções satisfatórias, apesar de fornecer informações importantes sobre as propriedades das posições de encaixe. Por outro lado, a segunda abordagem obteve resultados competitivos. O desempenho do algoritmo também foi compatível com outras soluções, inclusive em casos nos quais o volume de dados era alto. Ademais, como trabalho futuro, o algoritmo pode ser estendido de modo a possibilitar a entrada de itens de geometria genérica, o que pode se tornar o grande diferencial da proposta.

Método de desvio de obstáculos aplicado em veículo autônomo.

A operação de veículos autônomos necessita de meios para evitar colisões quando obstáculos não conhecidos previamente são interpostos em sua trajetória. Algoritmos para executar o desvio e sensores apropriados para a detecção destes obstáculos são essenciais para a operação destes veículos. Esta dissertação apresenta estudos sobre quatro algoritmos de desvio de obstáculos e tecnologia de três tipos de sensores aplicáveis à operação de veículos autônomos. Após os estudos teóricos, um dos algoritmos foi testado para a comprovação da aplicabilidade ao veículo de teste. A etapa experimental foi a realização de um programa, escrito em linguagem de programação Java, que aplicou o algoritmo Inseto 2 para o desvio de obstáculos em uma plataforma robótica (Robodeck) com o uso de sensores ultrassônicos embarcados na referida plataforma. Os experimentos foram conduzidos em ambiente fechado (indoor), bidimensional e horizontal (plano), fazendo o Robodeck executar uma trajetória. Para os testes, obstáculos foram colocados para simular situações variadas e avaliar a eficácia do algoritmo nestas configurações de caminho. O algoritmo executou o desvio dos obstáculos com sucesso e, quando havia solução para a trajetória, ela foi encontrada. Quando não havia solução, o algoritmo detectou esta situação e parou o veículo.

Modelo de otimização multiobjetivo aplicado ao projeto de concepção de submarinos convencionais.

Este trabalho apresenta um modelo de otimização multiobjetivo aplicado ao projeto de concepção de submarinos convencionais (i.e. de propulsão dieselelétrica). Um modelo de síntese que permite a estimativa de pesos, volume, velocidade, carga elétrica e outras características de interesse para a o projeto de concepção é formulado. O modelo de síntese é integrado a um modelo de otimização multiobjetivo baseado em algoritmos genéticos (especificamente, o algoritmo NSGA II). A otimização multiobjetivo consiste na maximização da efetividade militar do submarino e na minimização de seu custo. A efetividade militar do submarino é representada por uma Medida Geral de Efetividade (OMOE) estabelecida por meio do Processo Analítico Hierárquico (AHP). O Custo Básico de Construção (BCC) do submarino é estimado a partir dos seus grupos de peso. Ao fim do processo de otimização, é estabelecida uma Fronteira de Pareto composta por soluções não dominadas. Uma dessas soluções é selecionada para refinamento preliminar e os resultados são discutidos. Subsidiariamente, esta dissertação apresenta discussão sucinta sobre aspectos históricos e operativos relacionados a submarinos, bem como sobre sua metodologia de projeto. Alguns conceitos de Arquitetura Naval, aplicada ao projeto dessas embarcações, são também abordados.

Desenvolvimento de algoritmo de controle de tração para regeneração de energia metroviária - ACTREM: melhoria da eficiência energética de sistemas de tração metroviária.

Esta tese propõe um modelo de regeneração de energia metroviária, baseado no controle de paradas e partidas do trem ao longo de sua viagem, com o aproveitamento da energia proveniente da frenagem regenerativa no sistema de tração. O objetivo é otimizar o consumo de energia, promover maior eficiência, na perspectiva de uma gestão sustentável. Aplicando o Algoritmo Genético (GA) para obter a melhor configuração de tráfego dos trens, a pesquisa desenvolve e testa o Algoritmo de Controle de Tração para Regeneração de Energia Metroviária (ACTREM), usando a Linguagem de programação C++. Para analisar o desempenho do algoritmo de controle ACTREM no aumento da eficiência energética, foram realizadas quinze simulações da aplicação do ACTREM na linha 4 - Amarela do metrô da cidade de São Paulo. Essas simulações demonstraram a eficiência do ACTREM para gerar, automaticamente, os diagramas horários otimizados para uma economia de energia nos sistemas metroviários, levando em consideração as restrições operacionais do sistema, como capacidade máxima de cada trem, tempo total de espera, tempo total de viagem e intervalo entre trens. Os resultados mostram que o algoritmo proposto pode economizar 9,5% da energia e não provocar impactos relevantes na capacidade de transporte de passageiros do sistema. Ainda sugerem possíveis continuidades de estudos.

Metodologia para execução de aplicações paralelas baseadas no modelo BSP com tarefas heterogêneas.

A computação paralela permite uma série de vantagens para a execução de aplicações de grande porte, sendo que o uso efetivo dos recursos computacionais paralelos é um aspecto relevante da computação de alto desempenho. Este trabalho apresenta uma metodologia que provê a execução, de forma automatizada, de aplicações paralelas baseadas no modelo BSP com tarefas heterogêneas. É considerado no modelo adotado, que o tempo de computação de cada tarefa secundária não possui uma alta variância entre uma iteração e outra. A metodologia é denominada de ASE e é composta por três etapas: Aquisição (Acquisition), Escalonamento (Scheduling) e Execução (Execution). Na etapa de Aquisição, os tempos de processamento das tarefas são obtidos; na etapa de Escalonamento a metodologia busca encontrar a distribuição de tarefas que maximize a velocidade de execução da aplicação paralela, mas minimizando o uso de recursos, por meio de um algoritmo desenvolvido neste trabalho; e por fim a etapa de Execução executa a aplicação paralela com a distribuição definida na etapa anterior. Ferramentas que são aplicadas na metodologia foram implementadas. Um conjunto de testes aplicando a metodologia foi realizado e os resultados apresentados mostram que os objetivos da proposta foram alcançados.

Logística operacional: alocação de bases operacionais em distribuição de energia elétrica.

Ser eficiente é um requisito para a sustentabilidade das empresas concessionárias de distribuição de energia elétrica no Brasil. A busca pela eficiência deve estar em harmonia com a melhoria contínua da qualidade, da segurança e da satisfação dos consumidores e das partes envolvidas. O desafio de atender múltiplos objetivos requer que as empresas do setor desenvolvam soluções inovadoras, com a mudança de processos, tecnologia, estrutura e a capacitação das pessoas. Desenvolver um modelo operacional eficiente e uma gestão rigorosa dos custos são fatores-chave para o sucesso das empresas, considerando o contexto regulatório de revisão tarifária que incentiva a melhoria do desempenho. O modelo operacional é definido a partir da organização logística dos recursos para atendimento da demanda de serviços, que define também os custos fixos e variáveis de pessoal (salário, horas extras, refeições), infraestrutura (manutenção de prédios, ferramentas e equipamentos) e deslocamentos (manutenção de veículos, combustível), por exemplo. A melhor alocação e o melhor dimensionamento de bases operacionais possibilitam a redução dos custos com deslocamento e infraestrutura, favorecendo o aproveitamento da força de trabalho em campo, a melhoria do atendimento dos clientes e da segurança dos colaboradores. Este trabalho apresenta uma metodologia de otimização de custos através da alocação de bases e equipes operacionais, com o modelamento matemático dos objetivos e restrições do negócio e a aplicação de algoritmo evolutivo para busca das melhores soluções, sendo uma aplicação de Pesquisa Operacional, no campo da Localização de Instalações, em distribuição de energia elétrica. O modelo de otimização desenvolvido possibilita a busca pelo ponto de equilíbrio ótimo que minimiza o custo total formado pelos custos de infraestrutura, frota (veículos e deslocamentos) e pessoal. O algoritmo evolutivo aplicado no modelo oferece soluções otimizadas pelo melhoramento de conjuntos de variáveis binárias com base em conceitos da evolução genética. O modelo de otimização fornece o detalhamento de toda a estrutura operacional e de custos para uma determinada solução do problema, utilizando premissas de produtividade e deslocamentos (velocidades e distâncias) para definir as abrangências de atuação das bases operacionais, recursos (equipes, pessoas, veículos) necessários para atendimento da demanda de serviços, e projetar todos os custos fixos e variáveis associados. A metodologia desenvolvida neste trabalho considera também a projeção de demanda futura para a aplicação no estudo de caso, que evidenciou a efetividade da metodologia como ferramenta para a melhoria da eficiência operacional em empresas de distribuição de energia elétrica.

Otimização acústica e análise numérica do escoamento ao redor de um conjunto cilindro-placa separadora.

RESUMO Simulações de aeroacústica computacional demandam uma quantidade considerável de tempo, o que torna complicada a realização de estudos paramétricos. O presente trabalho propõe uma metodologia viável para otimização aeroacústica. Através da análise numérica utilizando dinâmica dos fluidos computacional, foi estudada a aplicação de uma placa separadora desacoplada como método de controle passivo da esteira turbulenta de um cilindro e avaliou-se a irradiação de ruído causado pela interação do escoamento com ambos os corpos, empregando ferramentas de aeroacústica computacional baseadas no método de Ffowcs-Williams e Hawkings. Algumas abordagens distintas de metodologias de otimização de projeto foram aplicadas neste problema, com o objetivo de chegar a uma configuração otimizada que permita a redução do nível sonoro ao longe. Assim, utilizando uma ferramenta de otimização multidisciplinar, pode-se avaliar a capacidade de modelos heurísticos e a grande vantagem do emprego de algoritmos baseados em método de superfície de resposta quando aplicados em um problema não linear, pois requerem a avaliação de um menor número de alternativas para se obter um ponto ótimo. Além disso, foi possível identificar e agrupar os resultados em 5 clusters baseados em seus parâmetros geométricos, nível de pressão sonora global e o valor quadrático médio do coeficiente de arrasto, confirmando a eficiência da aplicação de placas separadoras longas desacopladas posicionadas próximas ao cilindro na estabilização da esteira turbulenta, enquanto que o posicionamento de placas acima de um espaçamento crítico aumentou o nível de pressão acústica irradiado devido à formação de vórtices no espaço entre o cilindro e a placa separadora.

Simulación de procesos químicos (curso 2011-2012)

Apuntes en formato html que incluyen los siguientes temas de la parte de simulación en la asignatura «simulación y optimización de procesos químicos» TEMA 1. Introducción 1.1 Introducción. 1.2 Desarrollo histórico de la simulación de procesos. Relación entre simulación optimización y síntesis de procesos. 1.3 Tipos de simuladores: Modular secuencial. Modular simultáneo. Basada en ecuaciones. TEMA 2. Simulación Modular Secuencial 2.1 Descomposición de diagramas de flujo (flowsheeting) 2.2 Métodos basados en las matrices booleanas Localización de redes cíclicas máximas. Algoritmo de Sargent y Westerberg. Algoritmo de Tarjan. 2.3 Selección de las corrientes de corte: 2.3.1 Caso general planteamiento como un "set-covering problem" (algoritmo de Pho y Lapidus) 2.3.2 Número mínimo de corrientes de corte (algoritmo de Barkley y Motard) 2.3.3 Conjunto de corrientes de corte no redundante (Algoritmo de Upadhye y Grens) TEMA 3. Simulación Modular Simultánea 3.1 Efecto de las estrategias tipo cuasi Newton sobre la convergencia de los diagramas de flujo. TEMA 4. Simulación Basada en Ecuaciones 4.1 Introducción. Métodos de factorización de matrices dispersas. Métodos a priori y métodos locales. 4.2 Métodos locales: Criterio de Markowitz. 4.3 Métodos a priori: 4.3.1 Triangularización por bloques: a. Base de salida admisible (transversal completo). b. Aplicación de los algoritmos de Sargent y Tarjan a matrices dispersas. c. Reordenación. 4.3.2 Transformación en matriz triangular bordeada. 4.4 Fase numerica. Algoritmo RANKI 4.5 Comparación entre los diferentes sistemas de simulación. Ventajas e Inconvenientes. TEMA 5. Grados de libertad y variables de diseño de un diagrama de flujo 5.1 Teorema de Duhem y regla de las fases 5.2 Grados de libertad de un equipo 5.3 Grados de libertad de un diagrama de flujo 5.4 Elección de las variables de diseño.

Interoperabilidad semántica de ontologías basada en técnicas de procesamiento del lenguaje natural

Se presenta un estudio y propuesta de interoperabilidad semántica entre ontologías del dominio de la salud basada en técnicas de procesamiento del lenguaje natural. El objetivo fundamental ha sido el desarrollo de un algoritmo de interconexión semántica entre los términos de dos ontologías solapadas y heterogéneas, denominadas «fuente» (Clasificación internacional de enfermedades, 9ª revisión, modificación clínica: CIE-9-MC) y «diana» (esquema jerárquico de la asignatura Enfermería Materno-Infantil: EMI). Esta propuesta permite emparejar semánticamente ontologías, a partir de la reutilización de otro recurso ontológico (WordNet español), sin destruir o modificar la semántica de identidad de cada una de las ontologías involucradas. El modelo presentado puede permitir al usuario acceder a la información que necesita en otra clasificación jerárquica, sin precisar de un entrenamiento referido a la conceptualización de cada sistema, pues utilizaría la ontología «diana» con la que está familiarizado para su aplicación a la recuperación de información.

Estrategias para identificar oclusiones y planificación monocular para una mejora de la percepción visual de la escena

Esta Tesis doctoral está orientada al estudio de estrategias y técnicas para el tratamiento de oclusiones. Las oclusiones suponen uno de los principales problemas en la percepción de una escena mediante visión por computador. Las condiciones de luz, los puntos de vista con los que se captura información de la escena, las posiciones y orientaciones de los objetos presentes en la escena son algunas de las causas que provocan que los objetos puedan quedar ocluidos parcialmente. Las investigaciones expuestas en esta Tesis se pueden agrupar en función de su objetivo en dos grupos: técnicas cuya finalidad es detectar la presencia de oclusiones y estrategias que permiten mejorar la percepción de un sistema de visión por computador, aun en el caso de la presencia de oclusiones. En primer lugar, se han desarrollado una serie de técnicas orientadas a la detección de oclusiones a partir de procesos de extracción de características y de segmentación color en imágenes. Estas técnicas permiten definir qué regiones en la imagen son susceptibles de considerarse zonas de oclusión, debido a una mala percepción de la escena, como consecuencia de observarla con un mal punto de vista. Como aplicación de estas técnicas se han desarrollado algoritmos basados en la segmentación color de la imagen y en la detección de discontinuidades mediante luz estructurada. Estos algoritmos se caracterizan por no incluir conocimiento previo de la escena. En segundo lugar, se han presentado una serie de estrategias que permiten corregir y/o modificar el punto de vista de la cámara con la que se observa la escena. De esta manera, las oclusiones identificadas, mediante los métodos expuestos en la primera parte de la Tesis, y que generalmente son debidas a una mala localización de la cámara pueden ser eliminadas o atenuadas cambiando el punto de vista con el que se produce la observación. En esta misma línea se presentan dos estrategias para mejorar la posición y orientación espacial de la cámara cuando ésta se emplea para la captura de imágenes en procesos de reconocimiento. La primera de ellas se basa en la retroproyección de características obtenidas de una imagen real, a partir de una posición cualquiera, en imágenes virtuales correspondientes a las posibles posiciones que puede adoptar la cámara. Este algoritmo lleva a cabo la evaluación de un mapa de distancias entre estas características buscando en todo momento, maximizar estas distancias para garantizar un mejor punto de vista. La ventaja radica en que en ningún caso se hace necesario mover la cámara para determinar una nueva posición que mejore la percepción de la escena. La segunda de estas estrategias, busca corregir la posición de la cámara buscando la ortogonalidad. En este caso, se ha partido de la hipótesis inicial de que la mayor superficie visible siempre se suele conseguir situando la cámara ortogonalmente al plano en el que se sitúa el objeto.

An application of fuzzy logic for hardware/software partitioning in embedded systems

Hardware/Software partitioning (HSP) is a key task for embedded system co-design. The main goal of this task is to decide which components of an application are to be executed in a general purpose processor (software) and which ones, on a specific hardware, taking into account a set of restrictions expressed by metrics. In last years, several approaches have been proposed for solving the HSP problem, directed by metaheuristic algorithms. However, due to diversity of models and metrics used, the choice of the best suited algorithm is an open problem yet. This article presents the results of applying a fuzzy approach to the HSP problem. This approach is more flexible than many others due to the fact that it is possible to accept quite good solutions or to reject other ones which do not seem good. In this work we compare six metaheuristic algorithms: Random Search, Tabu Search, Simulated Annealing, Hill Climbing, Genetic Algorithm and Evolutionary Strategy. The presented model is aimed to simultaneously minimize the hardware area and the execution time. The obtained results show that Restart Hill Climbing is the best performing algorithm in most cases.

Optimización de áreas funcionales espaciales mediante algoritmos evolutivos multioperador. Aplicación a la delimitación de mercados locales de trabajo

El documento de esta tesis por compendio de publicaciones se divide en dos partes: la síntesis donde se resume la fundamentación, resultados y conclusiones de esta tesis, y las propias publicaciones en su formato original, que se incluyen como apéndices. Dado que existen acuerdo de confidencialidad (véase "Derechos" más adelante) que impiden su publicación en formato electrónico de forma pública y abierta (como es el repositorio de la UA), y acorde con lo que se dictamina en el punto 6 del artículo 14 del RD 99/2011, de 28 de enero, no se incluyen estos apéndices en el documento electrónico que se presenta en cedé, pero se incluyen las referencias completas y sí se incluyen integramente en el ejemplar encuadernado. Si el CEDIP y el RUA así lo decidiesen más adelante, podría modificarse este documento electrónico para incluir los enlaces a los artículos originales.

Partición hardware software de un codificador JPEG utilizando escalador de colinas estocástico

La partición hardware/software es una etapa clave dentro del proceso de co-diseño de los sistemas embebidos. En esta etapa se decide qué componentes serán implementados como co-procesadores de hardware y qué componentes serán implementados en un procesador de propósito general. La decisión es tomada a partir de la exploración del espacio de diseño, evaluando un conjunto de posibles soluciones para establecer cuál de estas es la que mejor balance logra entre todas las métricas de diseño. Para explorar el espacio de soluciones, la mayoría de las propuestas, utilizan algoritmos metaheurísticos; destacándose los Algoritmos Genéticos, Recocido Simulado. Esta decisión, en muchos casos, no es tomada a partir de análisis comparativos que involucren a varios algoritmos sobre un mismo problema. En este trabajo se presenta la aplicación de los algoritmos: Escalador de Colinas Estocástico y Escalador de Colinas Estocástico con Reinicio, para resolver el problema de la partición hardware/software. Para validar el empleo de estos algoritmos se presenta la aplicación de este algoritmo sobre un caso de estudio, en particular la partición hardware/software de un codificador JPEG. En todos los experimentos es posible apreciar que ambos algoritmos alcanzan soluciones comparables con las obtenidas por los algoritmos utilizados con más frecuencia.

Estudio y mejora de métodos de registro 3D: aceleración sobre unidades de procesamiento gráfico y caracterización del espacio de transformaciones iniciales

Durante los últimos años ha sido creciente el uso de las unidades de procesamiento gráfico, más conocidas como GPU (Graphic Processing Unit), en aplicaciones de propósito general, dejando a un lado el objetivo para el que fueron creadas y que no era otro que el renderizado de gráficos por computador. Este crecimiento se debe en parte a la evolución que han experimentado estos dispositivos durante este tiempo y que les ha dotado de gran potencia de cálculo, consiguiendo que su uso se extienda desde ordenadores personales a grandes cluster. Este hecho unido a la proliferación de sensores RGB-D de bajo coste ha hecho que crezca el número de aplicaciones de visión que hacen uso de esta tecnología para la resolución de problemas, así como también para el desarrollo de nuevas aplicaciones. Todas estas mejoras no solamente se han realizado en la parte hardware, es decir en los dispositivos, sino también en la parte software con la aparición de nuevas herramientas de desarrollo que facilitan la programación de estos dispositivos GPU. Este nuevo paradigma se acuñó como Computación de Propósito General sobre Unidades de Proceso Gráfico (General-Purpose computation on Graphics Processing Units, GPGPU). Los dispositivos GPU se clasifican en diferentes familias, en función de las distintas características hardware que poseen. Cada nueva familia que aparece incorpora nuevas mejoras tecnológicas que le permite conseguir mejor rendimiento que las anteriores. No obstante, para sacar un rendimiento óptimo a un dispositivo GPU es necesario configurarlo correctamente antes de usarlo. Esta configuración viene determinada por los valores asignados a una serie de parámetros del dispositivo. Por tanto, muchas de las implementaciones que hoy en día hacen uso de los dispositivos GPU para el registro denso de nubes de puntos 3D, podrían ver mejorado su rendimiento con una configuración óptima de dichos parámetros, en función del dispositivo utilizado. Es por ello que, ante la falta de un estudio detallado del grado de afectación de los parámetros GPU sobre el rendimiento final de una implementación, se consideró muy conveniente la realización de este estudio. Este estudio no sólo se realizó con distintas configuraciones de parámetros GPU, sino también con diferentes arquitecturas de dispositivos GPU. El objetivo de este estudio es proporcionar una herramienta de decisión que ayude a los desarrolladores a la hora implementar aplicaciones para dispositivos GPU. Uno de los campos de investigación en los que más prolifera el uso de estas tecnologías es el campo de la robótica ya que tradicionalmente en robótica, sobre todo en la robótica móvil, se utilizaban combinaciones de sensores de distinta naturaleza con un alto coste económico, como el láser, el sónar o el sensor de contacto, para obtener datos del entorno. Más tarde, estos datos eran utilizados en aplicaciones de visión por computador con un coste computacional muy alto. Todo este coste, tanto el económico de los sensores utilizados como el coste computacional, se ha visto reducido notablemente gracias a estas nuevas tecnologías. Dentro de las aplicaciones de visión por computador más utilizadas está el registro de nubes de puntos. Este proceso es, en general, la transformación de diferentes nubes de puntos a un sistema de coordenadas conocido. Los datos pueden proceder de fotografías, de diferentes sensores, etc. Se utiliza en diferentes campos como son la visión artificial, la imagen médica, el reconocimiento de objetos y el análisis de imágenes y datos de satélites. El registro se utiliza para poder comparar o integrar los datos obtenidos en diferentes mediciones. En este trabajo se realiza un repaso del estado del arte de los métodos de registro 3D. Al mismo tiempo, se presenta un profundo estudio sobre el método de registro 3D más utilizado, Iterative Closest Point (ICP), y una de sus variantes más conocidas, Expectation-Maximization ICP (EMICP). Este estudio contempla tanto su implementación secuencial como su implementación paralela en dispositivos GPU, centrándose en cómo afectan a su rendimiento las distintas configuraciones de parámetros GPU. Como consecuencia de este estudio, también se presenta una propuesta para mejorar el aprovechamiento de la memoria de los dispositivos GPU, permitiendo el trabajo con nubes de puntos más grandes, reduciendo el problema de la limitación de memoria impuesta por el dispositivo. El funcionamiento de los métodos de registro 3D utilizados en este trabajo depende en gran medida de la inicialización del problema. En este caso, esa inicialización del problema consiste en la correcta elección de la matriz de transformación con la que se iniciará el algoritmo. Debido a que este aspecto es muy importante en este tipo de algoritmos, ya que de él depende llegar antes o no a la solución o, incluso, no llegar nunca a la solución, en este trabajo se presenta un estudio sobre el espacio de transformaciones con el objetivo de caracterizarlo y facilitar la elección de la transformación inicial a utilizar en estos algoritmos.

Verificación de Sistemas Basada en Teoría de Tipos

Este proyecto se enmarca en la utlización de métodos formales (más precisamente, en la utilización de teoría de tipos) para garantizar la ausencia de errores en programas. Por un lado se plantea el diseño de nuevos algoritmos de chequeo de tipos. Para ello, se proponen nuevos algoritmos basados en la idea de normalización por evaluación que sean extensibles a otros sistemas de tipos. En el futuro próximo extenderemos resultados que hemos conseguido recientemente [16,17] para obtener: una simplificación de los trabajos realizados para sistemas sin regla eta (acá se estudiarán dos sistemas: a la Martin Löf y a la PTS), la formulación de estos chequeadores para sistemas con variables, generalizar la noción de categoría con familia utilizada para dar semántica a teoría de tipos, obtener una formulación categórica de la noción de normalización por evaluación y finalmente, aplicar estos algoritmos a sistemas con reescrituras. Para los primeros resultados esperados mencionados, nos proponemos como método adaptar las pruebas de [16,17] a los nuevos sistemas. La importancia radica en que permitirán tornar más automatizables (y por ello, más fácilmente utilizables) los asistentes de demostración basados en teoría de tipos. Por otro lado, se utilizará la teoría de tipos para certificar compiladores, intentando llevar adelante la propuesta nunca explorada de [22] de utilizar un enfoque abstracto basado en categorías funtoriales. El método consistirá en certificar el lenguaje "Peal" [29] y luego agregar sucesivamente funcionalidad hasta obtener Forsythe [23]. En este período esperamos poder agregar varias extensiones. La importancia de este proyecto radica en que sólo un compilador certificado garantiza que un programa fuente correcto se compile a un programa objeto correcto. Es por ello, crucial para todo proceso de verificación que se base en verificar código fuente. Finalmente, se abordará la formalización de sistemas con session types. Los mismos han demostrado tener fallas en sus formulaciones [30], por lo que parece conveniente su formalización. Durante la marcha de este proyecto, esperamos tener alguna formalización que dé lugar a un algoritmo de chequeo de tipos y a demostrar las propiedades usuales de los sistemas. La contribución es arrojar un poco de luz sobre estas formulaciones cuyos errores revelan que el tema no ha adquirido aún suficiente madurez o comprensión por parte de la comunidad.