Buscar
Mostrando ítems 1-10 de 306
Proof-term reconstruction from TSTP to Agda
(Universidad EAFITGrupo de investigación en Lógica y ComputaciónEscuela de Ciencias, 2015-12-19)
Proving compiler correctness using step-indexed logical relations
(2016)
In this paper we prove the correctness of a compiler for a call-by-name language using step-indexed logical relations and biorthogonality. The source language is an extension of the simply typed lambda-calculus with ...
A Mechanized Proof of a Textbook Type Unification Algorithm
(Instituto de Informática - Universidade Federal do Rio Grande do Sul, 2020)
A machine assisted proof of the subject reduction property for small typed functional language. Master Thesis
(UR. FI-INCO,, 1995)
We present an experiment in formally describing a programming language and its properties in constructive type theory. By constructive type theory we understand primarily the formulation of Martin Löf's set theory. ...
Formal Analysis of Security Models for Mobile Devices, Virtualization Platforms, and Domain Name Systems
(Centro Latinoamericano de Estudios en Informática, 2015)
A reasonably gradual type theory
(ACM, 2022)
Gradualizing the Calculus of Inductive Constructions (CIC) involves dealing with subtle tensions between normalization, graduality, and conservativity with respect to CIC. Recently, GCIC has been proposed as a parametrized ...
Juez inteligente. Expert system that assists the judge in the assessment of judicial proofJuez inteligente. Sistema experto que asiste al Juez en la valoración de la Prueba Judicial
(Pontificia Universidad Católica del Perú, 2021)
Formalization of context-free language theory
(Universidade Federal de PernambucoUFPEBrasilPrograma de Pos Graduacao em Ciencia da Computacao, 2016)
Formalizing alternating-time temporal logic in the coq proof assistant
(UR.FI-INCO, 2014)
This work presents a complete formalization of Alternating-time Temporal Logic (ATL) and its semantic model, Concurrent Game Structures (CGS), in the Calculus of (Co)Inductive Constructions, using the logical framework ...
An approach to subroutine elimination
(UR. FI – INCO., 2003)
Subroutines seem to be more a problem than a solution for the Byte Code Verifier's world, especially with resource constrained devices like Java Card. The elimination of subroutines form the Java bytecode would allow the ...