BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Departamento de Computación - ECPv6.15.18//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Departamento de Computación
X-ORIGINAL-URL:https://www.dc.uba.ar
X-WR-CALDESC:Eventos para Departamento de Computación
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:America/Sao_Paulo
BEGIN:STANDARD
TZOFFSETFROM:-0200
TZOFFSETTO:-0300
TZNAME:-03
DTSTART:20190217T020000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/Sao_Paulo:20200722T130000
DTEND;TZID=America/Sao_Paulo:20200722T150000
DTSTAMP:20260514T003816
CREATED:20200721T141005Z
LAST-MODIFIED:20200721T141005Z
UID:6021-1595422800-1595430000@www.dc.uba.ar
SUMMARY:Defensa Tesis Doctorado Andrés Viso
DESCRIPTION:Título: Un estudio semántico sobre extensiones avanzadas del λ-cálculo: patrones y operadores de control\nDirector: Eduardo Bonelli\nJurados:\n– Pablo Castro (Universidad Nacional de Río Cuarto\, Argentina)\n– Alejandro Díaz-Caro (Universidad Nacional de Quilmes e ICC\, FCEN-UBA\, Argentina)\n– Miguel Pagano (FAMAF\, Universidad Nacional de Córdoba\, Argentina) \nDónde: Zoom\, pero se transmitirá por streaming (el link se enviará un rato antes del comienzo de la defensa). \nResumen:\nEl siguiente trabajo presenta distintos análisis semánticos sobre fundamentos de lenguajes de programación funcional. En particular\, se establece como objeto de estudio el λ-cálculo para luego focalizar especialmente en dos de sus extensiones\, a saber: el Pure Pattern Calculus (PPC) y el λμ-cálculo de Parigot.\nEn un primer lugar se estudian estrategias de evaluación para λ-cálculo por medio del sistema de tipos intersección (no idempotente) V. El mismo es capaz de caracterizar (exactamente) los términos normalizantes. Esta herramienta permite establecer una igualdad observacional entre la conocida estrategia call-by-need –noción puramente sintáctica– y el concepto semántico de needed redexes.\nMás precisamente\, se introduce la reducción weak-head needed y se muestra que el sistema V identifica sintácticamente todos los redexes weak-head needed de un término.\nPPC\, introducido por Kesner y Jay\, es una extensión del λ-cálculo con patrones dinámicos y pattern matching que permite abstraer virtualmente cualquier término. Esto dio lugar a dos nuevas formas de polimorfirmo: path polymorphism y pattern polymorphism. El primero se refiere a la definición de funciones que se aplican uniformemente a estructuras de datos arbitrarias\, definidas de manera inductiva. Su escencia recae sobre patrones de la forma x y (i.e. la aplicación de dos variables)\, lo que permite descomponer una estructura de datos en sus diferentes partes. Este trabajo se enfoca en path polymorphism restringiendo el análisis al Calculus of Applicative Patterns (CAP)\, un nuevo formalismo que puede ser visto como el fragmento estático de PPC\, lo que descarta la forma de pattern polymorphism. Se desarrolla un sistema de tipos estático para CAP\, capaz de capturar path polymorphism mediante una combinación adecuada de\nherramientas de tipado como: tipos constantes\, aplicativos\, unión y recursivos.\nLas propiedades fundamentales de subject reduction y progress se satisfacen en el sistema propuesto\, lo que garantiza el buen comportamiento dinámico del cálculo. Esto recae crucialmente en una novedosa noción de compatibilidad de patrones. A su vez\, se desarrolla un algoritmo de type-checking eficiente median-\nte la formulación de una variante dirigida por sintaxis del sistema de tipos. Esto involucra algoritmos de chequeo de equivalencia de tipos y subtipado\, ambos basados en caracterizaciones coinductivas de estas relaciones.\nEn una tercera línea de investigación\, se consideran programas con operadores de control. El objetivo es identificar aquellos programas con tales constructores cuyas semánticas de reducción se corresponden de manera exacta. Esto se logra introduciendo una relación ≃\, definida sobre una presentación alternativa del λμ-cálculo con operadores explícitos llamada ΛM . El resultado se basa en dos ingredientes fundamentales: (1) la factorización de la reducción del λμ-cálculo en pasos multiplicativos y exponenciales mediante el uso de los nuevos\noperadores explícitos introducidos; y (2) la traducción de los términos de ΛM en las Polarized Proof-Nets (PPN) de Laurent\, de modo que cut-elimination en las PPN simula la reducción en ΛM. La relación ≃ propuesta caracteriza la equivalencia estructural de las PPN. Más aún\, ≃ resulta ser una bisimulación fuerte con respecto a la reducción en ΛM \, i.e. dos térmidos ≃-equivalentes tienen exactamente la misma semántica de reducción\, un resultado que falla tanto para la σ-equivalencia de Regnier en el λ-cálculo como para la σ-equivalencia de Laurent en el λμ-cálculo.
URL:https://www.dc.uba.ar/event/defensa-tesis-doctorado-andres-viso/
LOCATION:ZOOM
CATEGORIES:Agenda
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=America/Sao_Paulo:20200722T180000
DTEND;TZID=America/Sao_Paulo:20200722T190000
DTSTAMP:20260514T003816
CREATED:20200715T140223Z
LAST-MODIFIED:20200721T141246Z
UID:6001-1595440800-1595444400@www.dc.uba.ar
SUMMARY:Defensa Tesis Licenciatura Nicolás Chamo
DESCRIPTION:Título: «Análisis de cambios en los parámetros estructurales de bosques utilizando imágenes aéreas de VANTs»\nDirector: Francisco Gómez Fernández\nJurados: Facundo Pessacg (CONICET)\, Pablo De Cristóforis (DC-UBA)\, Sebastián Torrella (EGE-UBA)\n\nDía y hora: miércoles 22 de julio\, 18 hs\n\nLa misma será transmitida en tiempo real a través del siguiente link:\nhttps://www.youtube.com/watch?v=ijAAxUJMP6I\n\n\n\nResumen:\nEl análisis de los parámetros estructurales de bosques tiene múltiples aplicaciones en la gestión de bosques\, como por ejemplo en la elaboración de inventarios forestales. Por medio del estudio de los cambios a lo largo del tiempo de estos parámetros\, es también posible la evaluación del estado de conservación/degradación de estos bosques. Mediante el proceso de Structure from Motion (SFM)\, se analizan imágenes aéreas obtenidas desde VANTs para construir una nube de puntos 3D\, la cual luego es utilizada para generar modelos de superficie (DSM) y suelo (DTM). Al poseer estos modelos de dos vuelos de la misma área\, pero en momentos distintos\, es posible aplicar algoritmos especializados de detección de cambios con el objetivo de generar mapas geo-referenciados de cambios. \nGracias al desarrollo de un simulador de vuelo de vehículos aéreos no tripulados (VANT) en esta tesis\, se logró encontrar una combinación de configuraciones y parámetros de vuelo que mejoran la calidad de la nube de puntos 3D\, logrando una reducción de los errores entre 64% y 75%. Al mismo tiempo\, se desarrollaron nuevos algoritmos de aproximación de superficie del suelo\, logrando así reducir el error promedio de la reconstrucción del DTM en un 45% y la raíz del error cuadrático medio en un 57%. De esta forma\, mostramos que con buena reconstrucción 3D y estimación del suelo\, es posible detectar de forma correcta los cambios en los parámetros estructurales\, al exhibir casos de éxito tanto en las simulaciones\, como en ejemplos reales.
URL:https://www.dc.uba.ar/event/defensa-tesis-licenciatura-nicolas-chamo/
LOCATION:ZOOM
CATEGORIES:Agenda
END:VEVENT
END:VCALENDAR